Type arithmetic for cartesian product types
Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.
Created on 2022-01-26.
Last modified on 2023-09-11.
module foundation.type-arithmetic-cartesian-product-types where
Imports
open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import foundation-core.cartesian-product-types open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.propositions
Idea
We prove laws for the manipulation of cartesian products with respect to themselves and dependent pair types.
Laws
Commutativity of cartesian products
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where map-commutative-prod : A × B → B × A pr1 (map-commutative-prod (pair a b)) = b pr2 (map-commutative-prod (pair a b)) = a map-inv-commutative-prod : B × A → A × B pr1 (map-inv-commutative-prod (pair b a)) = a pr2 (map-inv-commutative-prod (pair b a)) = b is-section-map-inv-commutative-prod : (map-commutative-prod ∘ map-inv-commutative-prod) ~ id is-section-map-inv-commutative-prod (pair b a) = refl is-retraction-map-inv-commutative-prod : (map-inv-commutative-prod ∘ map-commutative-prod) ~ id is-retraction-map-inv-commutative-prod (pair a b) = refl is-equiv-map-commutative-prod : is-equiv map-commutative-prod is-equiv-map-commutative-prod = is-equiv-is-invertible map-inv-commutative-prod is-section-map-inv-commutative-prod is-retraction-map-inv-commutative-prod commutative-prod : (A × B) ≃ (B × A) pr1 commutative-prod = map-commutative-prod pr2 commutative-prod = is-equiv-map-commutative-prod
Associativity of cartesian products
module _ {l1 l2 l3 : Level} (A : UU l1) (B : UU l2) (C : UU l3) where map-associative-prod : (A × B) × C → A × (B × C) map-associative-prod = map-associative-Σ A (λ x → B) (λ w → C) map-inv-associative-prod : A × (B × C) → (A × B) × C map-inv-associative-prod = map-inv-associative-Σ A (λ x → B) (λ w → C) is-section-map-inv-associative-prod : (map-associative-prod ∘ map-inv-associative-prod) ~ id is-section-map-inv-associative-prod = is-section-map-inv-associative-Σ A (λ x → B) (λ w → C) is-retraction-map-inv-associative-prod : (map-inv-associative-prod ∘ map-associative-prod) ~ id is-retraction-map-inv-associative-prod = is-retraction-map-inv-associative-Σ A (λ x → B) (λ w → C) is-equiv-map-associative-prod : is-equiv map-associative-prod is-equiv-map-associative-prod = is-equiv-map-associative-Σ A (λ x → B) (λ w → C) associative-prod : ((A × B) × C) ≃ (A × (B × C)) associative-prod = associative-Σ A (λ x → B) (λ w → C)
The unit laws of cartesian product types with respect to contractible types
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (is-contr-B : is-contr B) where right-unit-law-prod-is-contr : (A × B) ≃ A right-unit-law-prod-is-contr = right-unit-law-Σ-is-contr (λ a → is-contr-B) module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (is-contr-A : is-contr A) where left-unit-law-prod-is-contr : (A × B) ≃ B left-unit-law-prod-is-contr = left-unit-law-Σ-is-contr is-contr-A (center is-contr-A) is-equiv-pr2-prod-is-contr : is-equiv (pr2 {B = λ a → B}) is-equiv-pr2-prod-is-contr = is-equiv-comp ( pr1) ( map-commutative-prod) ( is-equiv-map-commutative-prod) ( is-equiv-pr1-is-contr λ b → is-contr-A) equiv-pr2-prod-is-contr : (A × B) ≃ B pr1 equiv-pr2-prod-is-contr = pr2 pr2 equiv-pr2-prod-is-contr = is-equiv-pr2-prod-is-contr
Adding redundant property
equiv-add-redundant-prop : {l1 l2 : Level} {A : UU l1} {B : UU l2} → (is-prop B) → (f : A → B) → (A ≃ (A × B)) pr1 (equiv-add-redundant-prop is-prop-B f) a = a , f a pr2 (equiv-add-redundant-prop is-prop-B f) = is-equiv-is-invertible ( pr1) ( λ p → eq-pair refl (eq-is-prop is-prop-B)) ( λ a → refl)
See also
-
Functorial properties of cartesian products are recorded in
foundation.functoriality-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
. -
Arithmetical laws involving dependent pair types are recorded in
foundation.type-arithmetic-dependent-pair-types
.- Arithmetical laws involving dependent product types are recorded in
foundation.type-arithmetic-dependent-function-types
.
- Arithmetical laws involving dependent product types are recorded in
-
Arithmetical laws involving coproduct types are recorded in
foundation.type-arithmetic-coproduct-types
. -
Arithmetical laws involving the unit type are recorded in
foundation.type-arithmetic-unit-type
. -
Arithmetical laws involving the empty type are recorded in
foundation.type-arithmetic-empty-type
.
Recent changes
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).