Investigations on graph-theoretical constructions in Homotopy type theory

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

module foundations.HomotopyType where
open import foundations.TransportLemmas

module _
  {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {P : A → Type ℓ₂}
  where

Let (f , g : _{(x:A)} P(x)) be two sections of a type family (P : A ). A from (f) to (g) is a dependent function of type

[(f g) :_{(x : A)} (f(x) = g(x)).]

  homotopy
    : (f g : Π A P)
    ---------------
    → Type (ℓ₁ ⊔ ℓ₂)

  homotopy f g = ∀ (x : A) → f x ≡ g x

Usual notation for homotopy:

  _∼_ : (f g : ((x : A) → P x)) → Type (ℓ₁ ⊔ ℓ₂)
  f ∼ g = homotopy f g

  h-refl
    : (f : Π A P)
    -------------
    → f ∼ f

  h-refl f x = idp

  h-sym
    : (f g : Π A P)
    → f ∼ g
    -------
    → g ∼ f

  h-sym _ _ e x = ! (e x)

  h-comp
    : {f g h : Π A P}
    → f ∼ g
    → g ∼ h
    -------
    → f ∼ h

  h-comp u v x = (u x) · (v x)

Syntax:

  _●_
    : {f g h : Π A P}
    → f ∼ g
    → g ∼ h
    -------
    → f ∼ h

  α ● β = h-comp α β

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