# Equality of cartesian product types

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

Created on 2022-01-26.

module foundation.equality-cartesian-product-types where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-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.transport-along-identifications


## Idea

Identifications Id (pair x y) (pair x' y') in a cartesian product are equivalently described as pairs of identifications Id x x' and Id y y'. This provides us with a characterization of the identity type of cartesian product types.

## Definition

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

Eq-product : (s t : A × B) → UU (l1 ⊔ l2)
Eq-product s t = ((pr1 s) ＝ (pr1 t)) × ((pr2 s) ＝ (pr2 t))


## Properties

### The type Eq-product s t is equivalent to Id s t

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

eq-pair' : {s t : A × B} → Eq-product s t → s ＝ t
eq-pair' {pair x y} {pair .x .y} (pair refl refl) = refl

eq-pair :
{s t : A × B} → (pr1 s) ＝ (pr1 t) → (pr2 s) ＝ (pr2 t) → s ＝ t
eq-pair p q = eq-pair' (pair p q)

pair-eq : {s t : A × B} → s ＝ t → Eq-product s t
pr1 (pair-eq α) = ap pr1 α
pr2 (pair-eq α) = ap pr2 α

is-retraction-pair-eq :
{s t : A × B} → ((pair-eq {s} {t}) ∘ (eq-pair' {s} {t})) ~ id
is-retraction-pair-eq {pair x y} {pair .x .y} (pair refl refl) = refl

is-section-pair-eq :
{s t : A × B} → ((eq-pair' {s} {t}) ∘ (pair-eq {s} {t})) ~ id
is-section-pair-eq {pair x y} {pair .x .y} refl = refl

abstract
is-equiv-eq-pair :
(s t : A × B) → is-equiv (eq-pair' {s} {t})
is-equiv-eq-pair s t =
is-equiv-is-invertible pair-eq is-section-pair-eq is-retraction-pair-eq

equiv-eq-pair :
(s t : A × B) → Eq-product s t ≃ (s ＝ t)
pr1 (equiv-eq-pair s t) = eq-pair'
pr2 (equiv-eq-pair s t) = is-equiv-eq-pair s t

abstract
is-equiv-pair-eq :
(s t : A × B) → is-equiv (pair-eq {s} {t})
is-equiv-pair-eq s t =
is-equiv-is-invertible eq-pair' is-retraction-pair-eq is-section-pair-eq

equiv-pair-eq :
(s t : A × B) → (s ＝ t) ≃ Eq-product s t
pr1 (equiv-pair-eq s t) = pair-eq
pr2 (equiv-pair-eq s t) = is-equiv-pair-eq s t


### Commuting triangles for eq-pair

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

triangle-eq-pair :
{a0 a1 : A} {b0 b1 : B} (p : a0 ＝ a1) (q : b0 ＝ b1) →
eq-pair p q ＝ ((eq-pair p refl) ∙ (eq-pair refl q))
triangle-eq-pair refl refl = refl

triangle-eq-pair' :
{a0 a1 : A} {b0 b1 : B} (p : a0 ＝ a1) (q : b0 ＝ b1) →
eq-pair p q ＝ ((eq-pair refl q) ∙ (eq-pair p refl))
triangle-eq-pair' refl refl = refl


### eq-pair preserves concatenation

eq-pair-concat :
{l1 l2 : Level} {A : UU l1} {B : UU l2} {x x' x'' : A} {y y' y'' : B}
(p : x ＝ x') (p' : x' ＝ x'') (q : y ＝ y') (q' : y' ＝ y'') →
( eq-pair {s = pair x y} {t = pair x'' y''} (p ∙ p') (q ∙ q')) ＝
( ( eq-pair {s = pair x y} {t = pair x' y'} p q) ∙
( eq-pair p' q'))
eq-pair-concat refl p' refl q' = refl


### eq-pair computes in the expected way when the action on paths of the projections is applies

ap-pr1-eq-pair :
{l1 l2 : Level} {A : UU l1} {B : UU l2}
{x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
ap pr1 (eq-pair {s = pair x y} {pair x' y'} p q) ＝ p
ap-pr1-eq-pair refl refl = refl

ap-pr2-eq-pair :
{l1 l2 : Level} {A : UU l1} {B : UU l2}
{x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
ap pr2 (eq-pair {s = pair x y} {pair x' y'} p q) ＝ q
ap-pr2-eq-pair refl refl = refl


#### Computing transport along a path of the form eq-pair

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {a0 a1 : A} {b0 b1 : B}
where

tr-eq-pair :
(C : A × B → UU l3) (p : a0 ＝ a1) (q : b0 ＝ b1) (u : C (a0 , b0)) →
tr C (eq-pair p q) u ＝
tr (λ x → C (a1 , x)) q (tr (λ x → C (x , b0)) p u)
tr-eq-pair C refl refl u = refl


#### Computing transport along a path of the form eq-pair When one of the paths is refl

  left-unit-law-tr-eq-pair :
(C : A × B → UU l3) (q : b0 ＝ b1) (u : C (a0 , b0)) →
(tr C (eq-pair refl q) u) ＝ tr (λ x → C (a0 , x)) q u
left-unit-law-tr-eq-pair C refl u = refl

right-unit-law-tr-eq-pair :
(C : A × B → UU l3) (p : a0 ＝ a1) (u : C (a0 , b0)) →
(tr C (eq-pair p refl) u) ＝ tr (λ x → C (x , b0)) p u
right-unit-law-tr-eq-pair C refl u = refl


#### Computing transport along a path of the form eq-pair when both paths are identical

tr-eq-pair-diagonal :
{l1 l2 : Level} {A : UU l1} {a0 a1 : A} (C : A × A → UU l2)
(p : a0 ＝ a1) (u : C (a0 , a0)) →
tr C (eq-pair p p) u ＝ tr (λ a → C (a , a)) p u
tr-eq-pair-diagonal C refl u = refl