Equality of cartesian product types

{-# OPTIONS --safe #-}
module foundation-core.equality-cartesian-product-types where
Imports
open import foundation-core.cartesian-product-types
open import foundation-core.dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.functions
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.universe-levels

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-prod : (s t : A × B)  UU (l1  l2)
  Eq-prod s t = ((pr1 s)  (pr1 t)) × ((pr2 s)  (pr2 t))

Properties

The type Eq-prod 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-prod 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-prod s t
  pr1 (pair-eq α) = ap pr1 α
  pr2 (pair-eq α) = ap pr2 α

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

  issec-pair-eq :
    {s t : A × B}  ((eq-pair' {s} {t})  (pair-eq {s} {t})) ~ id
  issec-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-has-inverse pair-eq issec-pair-eq isretr-pair-eq

  equiv-eq-pair :
    (s t : A × B)  Eq-prod 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-has-inverse eq-pair' isretr-pair-eq issec-pair-eq

  equiv-pair-eq :
    (s t : A × B)  (s  t)  Eq-prod s t
  pr1 (equiv-pair-eq s t) = pair-eq
  pr2 (equiv-pair-eq s t) = is-equiv-pair-eq s t

Properties

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

See also