Functoriality of cartesian product types
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-01-26.
Last modified on 2024-04-25.
module foundation.functoriality-cartesian-product-types where
Imports
open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.morphisms-arrows open import foundation.universe-levels open import foundation-core.cartesian-product-types open import foundation-core.commuting-squares-of-maps open import foundation-core.contractible-maps open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types
Idea
The functorial action of the
cartesian product takes two maps
f : A → B
and g : C → D
and returns a map
f × g : A × B → C × D`
between the cartesian product types. This functorial action is bifunctorial in
the sense that for any two maps f : A → B
and g : C → D
the diagram
f×1
A × C ---> B × C
| \ |
1×g | \f×g | 1×g
| \ |
∨ ∨ ∨
A × D ---> B × D
f×1
commutes.
Definitions
The functorial action of cartesian product types
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} (f : A → B) (g : C → D) where map-product : (A × C) → (B × D) pr1 (map-product t) = f (pr1 t) pr2 (map-product t) = g (pr2 t) map-product-pr1 : pr1 ∘ map-product ~ f ∘ pr1 map-product-pr1 (a , c) = refl map-product-pr2 : pr2 ∘ map-product ~ g ∘ pr2 map-product-pr2 (a , c) = refl module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} (f : A → B) (g : C → D) where coherence-square-map-product : coherence-square-maps ( map-product f id) ( map-product id g) ( map-product id g) ( map-product f id) coherence-square-map-product t = refl
Properties
Functoriality of products preserves identity maps
map-product-id : {l1 l2 : Level} {A : UU l1} {B : UU l2} → map-product (id {A = A}) (id {A = B}) ~ id map-product-id (a , b) = refl
Functoriality of products preserves composition
preserves-comp-map-product : {l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6} (f : A → C) (g : B → D) (h : C → E) (k : D → F) → map-product (h ∘ f) (k ∘ g) ~ map-product h k ∘ map-product f g preserves-comp-map-product f g h k t = refl
Functoriality of products preserves homotopies
htpy-map-product : {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {f f' : A → C} (H : f ~ f') {g g' : B → D} (K : g ~ g') → map-product f g ~ map-product f' g' htpy-map-product H K (a , b) = eq-pair (H a) (K b)
Functoriality of products preserves equivalences
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} where map-inv-map-product : (f : A → C) (g : B → D) → is-equiv f → is-equiv g → C × D → A × B pr1 (map-inv-map-product f g H K (c , d)) = map-inv-is-equiv H c pr2 (map-inv-map-product f g H K (c , d)) = map-inv-is-equiv K d is-section-map-inv-map-product : (f : A → C) (g : B → D) (H : is-equiv f) (K : is-equiv g) → map-product f g ∘ map-inv-map-product f g H K ~ id is-section-map-inv-map-product f g H K = htpy-map-product ( is-section-map-inv-is-equiv H) ( is-section-map-inv-is-equiv K) is-retraction-map-inv-map-product : (f : A → C) (g : B → D) (H : is-equiv f) (K : is-equiv g) → map-inv-map-product f g H K ∘ map-product f g ~ id is-retraction-map-inv-map-product f g H K = htpy-map-product ( is-retraction-map-inv-is-equiv H) ( is-retraction-map-inv-is-equiv K) is-equiv-map-product : (f : A → C) (g : B → D) → is-equiv f → is-equiv g → is-equiv (map-product f g) is-equiv-map-product f g H K = is-equiv-is-invertible ( map-inv-map-product f g H K) ( is-section-map-inv-map-product f g H K) ( is-retraction-map-inv-map-product f g H K) equiv-product : A ≃ C → B ≃ D → A × B ≃ C × D pr1 (equiv-product (f , is-equiv-f) (g , is-equiv-g)) = map-product f g pr2 (equiv-product (f , is-equiv-f) (g , is-equiv-g)) = is-equiv-map-product f g is-equiv-f is-equiv-g
Functoriality of products preserves equivalences in either factor
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} where equiv-product-left : A ≃ C → A × B ≃ C × B equiv-product-left f = equiv-product f id-equiv equiv-product-right : B ≃ C → A × B ≃ A × C equiv-product-right = equiv-product id-equiv
The fibers of map-product f g
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} (f : A → C) (g : B → D) (t : C × D) where map-compute-fiber-map-product : fiber (map-product f g) t → fiber f (pr1 t) × fiber g (pr2 t) pr1 (pr1 (map-compute-fiber-map-product ((a , b) , refl))) = a pr2 (pr1 (map-compute-fiber-map-product ((a , b) , refl))) = refl pr1 (pr2 (map-compute-fiber-map-product ((a , b) , refl))) = b pr2 (pr2 (map-compute-fiber-map-product ((a , b) , refl))) = refl map-inv-compute-fiber-map-product : fiber f (pr1 t) × fiber g (pr2 t) → fiber (map-product f g) t pr1 (pr1 (map-inv-compute-fiber-map-product ((x , refl) , (y , refl)))) = x pr2 (pr1 (map-inv-compute-fiber-map-product ((x , refl) , (y , refl)))) = y pr2 (map-inv-compute-fiber-map-product ((x , refl) , (y , refl))) = refl is-section-map-inv-compute-fiber-map-product : map-compute-fiber-map-product ∘ map-inv-compute-fiber-map-product ~ id is-section-map-inv-compute-fiber-map-product ((x , refl) , (y , refl)) = refl is-retraction-map-inv-compute-fiber-map-product : map-inv-compute-fiber-map-product ∘ map-compute-fiber-map-product ~ id is-retraction-map-inv-compute-fiber-map-product ((a , b) , refl) = refl is-equiv-map-compute-fiber-map-product : is-equiv map-compute-fiber-map-product is-equiv-map-compute-fiber-map-product = is-equiv-is-invertible ( map-inv-compute-fiber-map-product) ( is-section-map-inv-compute-fiber-map-product) ( is-retraction-map-inv-compute-fiber-map-product) compute-fiber-map-product : fiber (map-product f g) t ≃ (fiber f (pr1 t) × fiber g (pr2 t)) pr1 compute-fiber-map-product = map-compute-fiber-map-product pr2 compute-fiber-map-product = is-equiv-map-compute-fiber-map-product
If map-product f g : A × B → C × D
is an equivalence, then we have D → is-equiv f
and C → is-equiv g
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} (f : A → C) (g : B → D) where is-equiv-left-factor-is-equiv-map-product' : D → is-equiv (map-product f g) → is-equiv f is-equiv-left-factor-is-equiv-map-product' d is-equiv-fg = is-equiv-is-contr-map ( λ x → is-contr-left-factor-product ( fiber f x) ( fiber g d) ( is-contr-is-equiv' ( fiber (map-product f g) (x , d)) ( map-compute-fiber-map-product f g (x , d)) ( is-equiv-map-compute-fiber-map-product f g (x , d)) ( is-contr-map-is-equiv is-equiv-fg (x , d)))) is-equiv-right-factor-is-equiv-map-product' : C → is-equiv (map-product f g) → is-equiv g is-equiv-right-factor-is-equiv-map-product' c is-equiv-fg = is-equiv-is-contr-map ( λ y → is-contr-right-factor-product ( fiber f c) ( fiber g y) ( is-contr-is-equiv' ( fiber (map-product f g) (c , y)) ( map-compute-fiber-map-product f g (c , y)) ( is-equiv-map-compute-fiber-map-product f g (c , y)) ( is-contr-map-is-equiv is-equiv-fg (c , y))))
The functorial action of products on arrows
Given a pair of morphisms of arrows
α : f → g
and β : h → i
, there is an induced morphism of arrows
α × β : f × h → g × i
and this construction is functorial.
module _ {l1 l2 l3 l4 l5 l6 l7 l8 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {C : UU l5} {D : UU l6} {Z : UU l7} {W : UU l8} (f : A → B) (g : X → Y) (h : C → D) (i : Z → W) (α : hom-arrow f g) (β : hom-arrow h i) where product-hom-arrow : hom-arrow (map-product f h) (map-product g i) product-hom-arrow = ( ( map-product ( map-domain-hom-arrow f g α) ( map-domain-hom-arrow h i β)) , ( map-product ( map-codomain-hom-arrow f g α) ( map-codomain-hom-arrow h i β)) , ( htpy-map-product ( coh-hom-arrow f g α) ( coh-hom-arrow h i β)))
See also
- Arithmetical laws involving cartesian product types are recorded in
foundation.type-arithmetic-cartesian-product-types
. - Equality proofs in cartesian product types are characterized in
foundation.equality-cartesian-product-types
. - The universal property of cartesian product types is treated in
foundation.universal-property-cartesian-product-types
. - Functorial properties of dependent pair types are recorded in
foundation.functoriality-dependent-pair-types
. - Functorial properties of dependent product types are recorded in
foundation.functoriality-dependent-function-types
. - Functorial properties of coproduct types are recorded in
foundation.functoriality-coproduct-types
.
Recent changes
- 2024-04-25. Fredrik Bakke. chore: Fix arrowheads in character diagrams (#1124).
- 2024-03-22. Fredrik Bakke. Additions to cartesian morphisms (#1087).
- 2024-03-20. Fredrik Bakke. Janitorial work on equivalences and embeddings (#1085).
- 2024-03-02. Fredrik Bakke. Factor out standard pullbacks (#1042).
- 2024-03-01. Fredrik Bakke. chore: Fix markdown list formatting (#1047).