Investigations on graph-theoretical constructions in Homotopy type theory

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

module foundations.CoproductIdentities where
open import foundations.BasicTypes
open import foundations.BasicFunctions
open import foundations.Transport
open import foundations.TransportLemmas

Coproduct identities and extra ∑-lemmas

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

∑-≡ B idp idp = idp

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

π₁-≡ B idp = idp

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

π₂-≡ B idp = idp

∑-map
  :  ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂}
  → {A' : Type ℓ₃} {B' : A' → Type ℓ₄}
  → (f : A → A')
  → ((a : A) → B a → B' (f a))
  ----------------------------
  → ∑ A B → ∑ A' B'

∑-map f g p = (f (π₁ p) , g (π₁ p) (π₂ p))

∑-map-compose
  : ∀ {i₀ j₀ i₁ j₁ i₂ j₂}
  → {A₀ : Type i₀} {B₀ : A₀ → Type j₀}
  → {A₁ : Type i₁} {B₁ : A₁ → Type j₁}
  → {A₂ : Type i₂} {B₂ : A₂ → Type j₂}
  → (f₀ : A₀ → A₁) → (f₁ : (a : A₀) → B₀ a → B₁ (f₀ a))
  → (g₀ : A₁ → A₂) → (g₁ : (a : A₁) → B₁ a → B₂ (g₀ a))
  → (x : ∑ A₀ B₀)
  -------------------------------------------------------
  → ∑-map (g₀ ∘ f₀) (λ a b → g₁ (f₀ a) (f₁ a b)) x
  ≡ (∑-map {B' = B₂} g₀ g₁ (∑-map {B' = B₁} f₀ f₁ x))

∑-map-compose _ _ _ _ (a , b) = idp

∑-lift
  :  ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂} {C : A → Type ℓ₂}
  → (∀ a → B a → C a)
  --------------------
  → ∑ A B → ∑ A C

∑-lift f = ∑-map id f

Some of the following identities are a customized version of the lemmas above.

module Sigma {ℓᵢ ℓⱼ} {A : Type ℓᵢ} {P : A → Type ℓⱼ} where

Two dependent pairs are equal if they are componentwise equal.

  Σ-componentwise
    : ∀ {v w : Σ A P}
    → v ≡ w
    ----------------------------------------------
    → Σ (π₁ v ≡ π₁ w) (λ p → tr P p (π₂ v) ≡ π₂ w)

  Σ-componentwise  idp = (idp , idp)

  Σ-bycomponents
    : ∀ {v w : Σ A P}
    → Σ (π₁ v ≡ π₁ w) (λ p → (π₂ v) ≡ (π₂ w) [ P ↓ p ] )
    -----------------------------------------------
    → v ≡ w

  Σ-bycomponents (idp , idp) = idp

Synonym of Σ-bycomponents:

  pair= = Σ-bycomponents

A trivial consequence is the following identification:

  lift-pair=
    : ∀ {x y : A} {u : P x}
    → (p : x ≡ y)
    --------------------------------------------------------
    → lift {A = A}{C = P} p  u ≡ pair= (p , refl (tr P p u))

  lift-pair= idp = idp

Uniqueness principle property for products

  uppt : (x : Σ A P) → (π₁ x , π₂ x) ≡ x
  uppt (a , b) = idp

  Σ-ap-π₁
    : ∀ {a₁ a₂ : A} {b₁ : P a₁} {b₂ : P a₂}
    → (α : a₁ ≡ a₂)
    → (γ : b₁ ≡ b₂ [ P ↓ α ])
    ------------------------------
    → ap π₁ (pair= (α , γ)) ≡ α

  Σ-ap-π₁ idp idp = idp
  ap-π₁-pair= = Σ-ap-π₁

  ap-π₁-!pair=
    : ∀ {a₁ a₂ : A} {b₁ : P a₁} {b₂ : P a₂}
    → (α : a₁ ≡ a₂)
    → (γ : b₁ ≡ b₂ [ P ↓ α ])
    ------------------------------
    → ap π₁ (! (pair= (α , γ))) ≡ (! α)

  ap-π₁-!pair= idp idp = idp

open Sigma public

transport-fun-dependent-bezem
  : ∀ {ℓᵢ ℓⱼ} {X : Type ℓᵢ} {A : X → Type ℓⱼ}
      {B : (x : X) → (a : A x) → Type ℓⱼ} {x y : X}
  → (p : x ≡ y)
  → (f : (a : A x) → B x a)
  → (a' : A y)
  ----------------------------------------------------------
  → (tr (λ x → (a : A x) → B x a) p f) a'
    ≡ tr (λ w → B (π₁ w) (π₂ w))
          (pair= (p , transport-inv p )) (f (tr A (! p) a'))

transport-fun-dependent-bezem idp f a' = idp

{- The following I found it in HoTT-Agda, very convenient lemma -}
module _ {i j k} {A : Type i} {B : A → Type j} {C : (a : A) → B a → Type k}
   where

   ↓-Σ-in : {x x' : A} {p : x ≡ x'} {r : B x} {r' : B x'}
     {s : C x r} {s' : C x' r'}
     (q : r ≡ r' [ B ↓ p ])
     → s ≡ s' [ uncurry C ↓ pair= (p , q) ]
     → (r , s) ≡ (r' , s') [ (λ x → Σ (B x) (C x)) ↓ p ]
   ↓-Σ-in {p = idp} idp t = pair= (idp , t)

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