# 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-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


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