Investigations on graph-theoretical constructions in Homotopy type theory

{-# OPTIONS --without-K --exact-split #-}
module foundations.AlgebraOnDependentPaths where

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

!ᵈ
  : ∀ {ℓ₁ ℓ₂}{A : Type ℓ₁} {B : A → Type ℓ₂} {x y : A}
  → {p : x ≡ y} {u : B x} {v : B y}
  → u ≡ v [ B ↓ p ]
  ---------------------
  → v ≡ u [ B ↓ (! p)]

!ᵈ {p = idp} = !_

↓-cst-in : {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : Type ℓ₂} {x y : A} {p : x ≡ y} {u v : B}
  → u ≡ v
  → u ≡ v [ (λ _ → B) ↓ p ]
↓-cst-in {p = idp} q = q

↓-cst-out : {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : Type ℓ₂}  {x y : A} {p : x ≡ y} {u v : B}
  → u ≡ v [ (λ _ → B) ↓ p ]
  → u ≡ v
↓-cst-out {p = idp} q = q

_·2ᵈ_
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂}
  → {f g h : Π A B}
  → {a a' : A} {p : a ≡ a'} {q : f a ≡ g a} {q' : f a' ≡ g a'}
  → {r : g a ≡ h a} {r' : g a' ≡ h a'}
  → (q ≡ q'           [ (λ a → f a ≡ g a) ↓ p ])
  → (r ≡ r'           [ (λ a → g a ≡ h a) ↓ p ])
  ------------------------------------------------
  → (q · r ≡ q' · r' [ (λ a → f a ≡ h a) ↓ p ])

_·2ᵈ_ {p = idp} idp idp = idp -- α · β

apd-·
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂}
  → (f : ∏ A B) → {a₁ a₂ a₃ : A}
  → (α : a₁ ≡ a₂) → (β : a₂ ≡ a₃)
  -----------------------------------------------------------------
  → apd f (α · β) ≡ pathover-comp {p = α} (apd f α) (apd f β)

apd-· C idp idp = idp

apd-!
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂}
  → (f : ∏ A B) → {a₁ a₂ : A}
  → (α : a₁ ≡ a₂)
  ----------------------------------------------------------------------------
  → apd f (α ⁻¹) ≡  ! (move-transport {α = α} (apd f α))

apd-! C idp = idp

·d-lunit
  : ∀ {ℓ₁ ℓ₂ : Level}
  → {A : Type ℓ₁} {B : A → Type ℓ₂} {x y : A}{p : x ≡ y}
  → {u : B x} {v : B y}
  → (r : u ≡ v [ B ↓ p ])
  ------------------------
  → pathover-comp {q = p} idp r ≡ r
·d-lunit {p = 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