Investigations on graph-theoretical constructions in Homotopy type theory

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

module foundations.HomotopyLemmas where
open import foundations.Transport
open import foundations.HomotopyType

hl-comp
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁}{B : Type ℓ₂} {C : Type ℓ₃}
  → {f g : A → B}
  → {j k : B → C}
  → f ∼ g
  → j ∼ k
  -------------------
  → (j ∘ f) ∼ (k ∘ g)

hl-comp {g = g}{j = j} f-g j-k = λ x → ap j (f-g x) · j-k (g x)

rcomp-∼
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁}{B : Type ℓ₂} {C : Type ℓ₃}
  → (f : A → B)
  → {j k : B → C}
  → j ∼ k
  -------------------
  → (j ∘ f) ∼ (k ∘ f)

rcomp-∼ f j-k = hl-comp (h-refl f) j-k

lcomp-∼
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁}{B : Type ℓ₂} {C : Type ℓ₃}
  → {f g : A → B}
  → (j : B → C)
  → f ∼ g
  -------------------
  → (j ∘ f) ∼ (j ∘ g)

lcomp-∼ j α = hl-comp α (h-refl j)

Homotopy is natural, meaning that it satisfies the following square commutative diagram.

h-naturality
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂}
  → {f g : A → B} → {x y : A}
  → (H : f ∼ g)
  → (p : x ≡ y)
  ------------------------------
  → H x · ap g p ≡ ap f p · H y

h-naturality {x = x} H idp = ! (·-runit (H x))

A particular case of naturality on the identity function.

h-naturality-id
  : ∀ {ℓ : Level} {A : Type ℓ}  {f : A → A} → {x : A}
  → (H : f ∼ id)
  -----------------------
  → H (f x) ≡ ap f (H x)

h-naturality-id {f = f} {x = x} H =
  begin
    H (f x)
      ≡⟨ ·-runit (H (f x)) ⟩
    H (f x) · refl (f x)
      ≡⟨ ap (H (f x) ·_) (! (·-rinv (H x))) ⟩
    H (f x) · ((H x) · (! (H x)))
      ≡⟨ ap (H (f x) ·_) (ap (_· (! (H x))) (! ap-id (H x))) ⟩
    H (f x) · (ap id (H x) · ! (H x))
      ≡⟨ ! (·-assoc (H (f x)) (ap id (H x)) (! (H x))) ⟩
    (H (f x) · ap id (H x)) · ! (H x)
      ≡⟨ ·-right-to-left-r (h-naturality H (H x)) ⟩
    ap f (H x)
  ∎

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