Investigations on graph-theoretical constructions in Homotopy type theory

{-# OPTIONS --without-K --exact-split #-}

module foundations.ProductIdentities where

open import foundations.BasicTypes public
open import foundations.BasicFunctions public
open import foundations.Transport public

prodComponentwise
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂} {x y : A × B}
  → (x ≡ y)
  ---------------------------------
  → (π₁ x ≡ π₁ y) × (π₂ x ≡ π₂ y)

prodComponentwise {x = x} idp = refl (π₁ x) , refl (π₂ x)

:

prodByComponents
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂} {x y : A × B}
  → (π₁ x ≡ π₁ y) × (π₂ x ≡ π₂ y)
  ---------------------------------
  → (x ≡ y)

prodByComponents {x = a , b} (idp , idp) = refl (a , b)

:

prodCompInverse
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂} {x y : A × B}
  → (b : (π₁ x ≡ π₁ y) × (π₂ x ≡ π₂ y))
  ---------------------------------------------
  → prodComponentwise (prodByComponents b) ≡ b

prodCompInverse {x = x} (idp , idp) = refl (refl (π₁ x) , refl (π₂ x))

:

prodByCompInverse
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂}  {x y : A × B}
  → (b : x ≡ y)
  ---------------------------------------------
  → prodByComponents (prodComponentwise b) ≡ b

prodByCompInverse {x = x} idp = refl (refl x)

×-≡
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂}
  → {ab ab' : A × B}
  → (p : π₁ ab ≡ π₁ ab') → (π₂ ab) ≡ π₂ ab'
  → ab ≡ ab'

×-≡ idp idp = idp

Latest changes

(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides
(2022-07-06)(d3a4a8cf) minors by jonathan.cubides
(2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides
(2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides
(2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides
(2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides
(2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides
(2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides
(2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides
(2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides
(2021-12-15)(0630ce66) Minor fixes by jonathan.cubides
(2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides
(2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides
(2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides
(2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides