Investigations on graph-theoretical constructions in Homotopy type theory

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

module foundations.Transport where

open import foundations.BasicTypes public
open import foundations.AlgebraOnPaths public

transport
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}
  → (C : A → Type ℓ₂) {a₁ a₂ : A}
  → (p : a₁ ≡ a₂)
  -------------------------------
  → (C a₁ → C a₂)

transport C idp = (λ x → x)

More syntax:

tr     = transport
tr₁    = transport
transp = transport

coe
  : ∀ {ℓ : Level} {A B : Type ℓ}
  → A ≡ B
  ---------
  → (A → B)

coe p a = tr (λ X → X) p a

and its inverse:

!coe
  : ∀ {ℓ : Level} {A B : Type ℓ}
  → A ≡ B
  ---------
  → (B → A)

!coe p a = tr (λ X → X) (! p) a

Let be , , , and . Using the same notation from {% cite hottbook %}, one of the definitions for the Pathover type is as the shorthand for the path between the tr along a path of the point and the point in the fiber . That is, a pathover is a term that inhabit the type also denoted by .

PathOver
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}
  → (B : A → Type ℓ₂) {a₁ a₂ : A}
  → (b₁ : B a₁) → (α : a₁ ≡ a₂) → (b₂ : B a₂)
  --------------------------------------------
  → Type ℓ₂

PathOver B b₁ α b₂ = tr B α b₁ ≡ b₂

infix  PathOver

syntax PathOver B b₁ α b₂  = b₁ ≡ b₂ [ B ↓ α ]

Another notation:

≡Over = PathOver

infix  ≡Over
syntax ≡Over B b α b' = b ≡ b' [ B / α ]

infixl  _·d_
_·d_
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂}
  → {a₁ a₂ a₃ : A} {p : a₁ ≡ a₂} {q : a₂ ≡ a₃}
  → {b₁ : B a₁}{b₂ : B a₂} {b₃ : B a₃}
  → (b₁ ≡ b₂ [ B / p ])
  → (b₂ ≡ b₃ [ B / q ])
  -------------------------
  → b₁ ≡ b₃ [ B / (p · q) ]

_·d_ {p = idp} {q = idp} idp idp = idp -- α β = α · β

pathover-comp = _·d_
_∙d_          = _·d_

tr₁-≡
  : ∀ {ℓ : Level} {A : Type ℓ} {a₀ a₁ a₂ : A}
  → (α : a₁ ≡ a₂)
  → (ε : a₀ ≡ a₁)
  → (δ : a₀ ≡ a₂)
  → (ε ≡ δ [ (λ a' → a₀ ≡ a') / α ])
  ----------------------------------
  → α ≡ ! ε · δ

tr₁-≡ idp .idp idp idp = idp

tr₂
  :  ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂}
  → (C : (a : A) → (B a → Type ℓ₃))
  → {a₁ a₂ : A}{b₁ : B a₁}{b₂ : B a₂}
  → (p : a₁ ≡ a₂)
  → (q : b₁ ≡ b₂ [ B ↓ p ])
  → C a₁ b₁
  -----------------------
  → C a₂ b₂

tr₂ C idp idp = id

Gylterud’s tr₂-commute:

:

tr₂-commute
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂}
  → (C : (a : A) → (B a → Type ℓ₃))
  → (D : (a : A) → (B a → Type ℓ₃))
  → (f : ∀ a b → C a b → D a b)
  → ∀ {a a' b b'}
  → (p : a ≡ a')
  → (q : b ≡ b' [ B / p ])
  ---------------------------------------------------
  → ∀ c → tr₂ D p q (f a b c) ≡ f a' b' (tr₂ C p q c)

tr₂-commute C D f idp idp c = 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