# Type arithmetic for cartesian product types

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-01-26.

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-product : A × B → B × A
pr1 (map-commutative-product (pair a b)) = b
pr2 (map-commutative-product (pair a b)) = a

map-inv-commutative-product : B × A → A × B
pr1 (map-inv-commutative-product (pair b a)) = a
pr2 (map-inv-commutative-product (pair b a)) = b

is-section-map-inv-commutative-product :
(map-commutative-product ∘ map-inv-commutative-product) ~ id
is-section-map-inv-commutative-product (pair b a) = refl

is-retraction-map-inv-commutative-product :
(map-inv-commutative-product ∘ map-commutative-product) ~ id
is-retraction-map-inv-commutative-product (pair a b) = refl

is-equiv-map-commutative-product : is-equiv map-commutative-product
is-equiv-map-commutative-product =
is-equiv-is-invertible
map-inv-commutative-product
is-section-map-inv-commutative-product
is-retraction-map-inv-commutative-product

commutative-product : (A × B) ≃ (B × A)
pr1 commutative-product = map-commutative-product
pr2 commutative-product = is-equiv-map-commutative-product


### Associativity of cartesian products

module _
{l1 l2 l3 : Level} (A : UU l1) (B : UU l2) (C : UU l3)
where

map-associative-product : (A × B) × C → A × (B × C)
map-associative-product = map-associative-Σ A (λ _ → B) (λ _ → C)

map-inv-associative-product : A × (B × C) → (A × B) × C
map-inv-associative-product = map-inv-associative-Σ A (λ _ → B) (λ _ → C)

is-section-map-inv-associative-product :
(map-associative-product ∘ map-inv-associative-product) ~ id
is-section-map-inv-associative-product =
is-section-map-inv-associative-Σ A (λ _ → B) (λ _ → C)

is-retraction-map-inv-associative-product :
(map-inv-associative-product ∘ map-associative-product) ~ id
is-retraction-map-inv-associative-product =
is-retraction-map-inv-associative-Σ A (λ _ → B) (λ _ → C)

is-equiv-map-associative-product : is-equiv map-associative-product
is-equiv-map-associative-product =
is-equiv-map-associative-Σ A (λ _ → B) (λ _ → C)

associative-product : ((A × B) × C) ≃ (A × (B × C))
associative-product = associative-Σ A (λ _ → B) (λ _ → 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-product-is-contr : A × B ≃ A
right-unit-law-product-is-contr = right-unit-law-Σ-is-contr (λ _ → is-contr-B)

inv-right-unit-law-product-is-contr : A ≃ A × B
inv-right-unit-law-product-is-contr =
inv-equiv right-unit-law-product-is-contr

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (is-contr-A : is-contr A)
where

left-unit-law-product-is-contr : A × B ≃ B
left-unit-law-product-is-contr =
left-unit-law-Σ-is-contr is-contr-A (center is-contr-A)

inv-left-unit-law-product-is-contr : B ≃ A × B
inv-left-unit-law-product-is-contr = inv-equiv left-unit-law-product-is-contr

is-equiv-pr2-product-is-contr : is-equiv (pr2 {B = λ _ → B})
is-equiv-pr2-product-is-contr =
is-equiv-comp
( pr1)
( map-commutative-product)
( is-equiv-map-commutative-product)
( is-equiv-pr1-is-contr (λ _ → is-contr-A))

equiv-pr2-product-is-contr : (A × B) ≃ B
pr1 equiv-pr2-product-is-contr = pr2
pr2 equiv-pr2-product-is-contr = is-equiv-pr2-product-is-contr


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