Investigations on graph-theoretical constructions in Homotopy type theory

{-# OPTIONS --without-K --exact-split #-}
module foundations.AlgebraOnPaths where
open import foundations.BasicTypes public
open import foundations.BasicFunctions public

ap²
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁}{B : Type ℓ₂} {C : Type ℓ₃}  {a₁ a₂ : A} {b₁ b₂ : B}
  → (f : A → B → C)
  → (a₁ ≡ a₂) → (b₁ ≡ b₂)
  --------------------------
  → f a₁ b₁  ≡ f a₂ b₂

ap² f idp idp = idp

ap-·
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂} {a b c : A}
  → (f : A → B) → (p : a ≡ b) → (q : b ≡ c)
  -------------------------------------------
  → ap f (p · q) ≡ ap f p · ap f q

ap-· f idp q = refl (ap f q)

ap-inv
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂}  {a b : A}
  → (f : A → B) → (p : a ≡ b)
  ----------------------------
  → ap f (p ⁻¹) ≡ (ap f p) ⁻¹

ap-inv f idp = idp
ap-! = ap-inv

ap-comp
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁}{B : Type ℓ₂} {C : Type ℓ₃} {a b : A}
  → (f : A → B)
  → (g : B → C)
  → (p : a ≡ b)
  -------------------------------
  → ap g (ap f p) ≡ ap (g ∘ f) p

ap-comp f g idp = idp

ap-id
  : ∀ {ℓ : Level} {A : Type ℓ} {a b : A}
  → (p : a ≡ b)
  --------------
  → ap id p ≡ p

ap-id idp = idp

ap-const
  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁}{B : Type ℓ₂}  {a a' : A} {b : B}
  → (p : a ≡ a')
  -----------------------
  → ap (λ _ → b) p ≡ idp

ap-const {b = b} idp = refl (refl b)

·-runit
  : ∀ {ℓ : Level} {A : Type ℓ}  {a a' : A}
  → (p : a ≡ a')
  --------------
  → p ≡ p · idp

·-runit idp = idp

·-lunit
  : ∀ {ℓ : Level} {A : Type ℓ}  {a a' : A}
  → (p : a ≡ a')
  --------------
  → p ≡ idp · p

·-lunit idp = idp

·-linv
  : ∀ {ℓ : Level} {A : Type ℓ}  {a a' : A}
  → (p : a ≡ a')
  ----------------
  → ! p · p ≡ idp

·-linv idp = idp

≡-inverse-left = ·-linv

·-rinv
  : ∀ {ℓ : Level} {A : Type ℓ}  {a a' : A}
  → (p : a ≡ a')
  ----------------
  → p · ! p ≡ idp

·-rinv idp = idp

≡-inverse-right  = ·-rinv

involution
  : ∀ {ℓ : Level} {A : Type ℓ}  {a a' : A}
  → (p : a ≡ a')
  ---------------
  → ! (! p) ≡ p

involution idp = idp

·-assoc
  : ∀ {ℓ : Level} {A : Type ℓ} {a b c d : A}
  → (p : a ≡ b) → (q : b ≡ c) → (r : c ≡ d)
  --------------------------------------------
  → p · q · r ≡ p · (q · r)

·-assoc idp q r = idp

·-cancellation
  : ∀ {ℓ : Level} {A : Type ℓ} {a : A}
  → (p : a ≡ a) → (q : a ≡ a)
  → p · q ≡ p
  -----------------------------------------
  → q ≡ refl a

·-cancellation {a = a} p q α =
    begin
      q               ≡⟨ ap (_· q) (! (·-linv p)) ⟩
      (! p · p) · q   ≡⟨ (·-assoc (! p) p q) ⟩
      ! p · (p · q)   ≡⟨ ap (! p ·_) α ⟩
      ! p · p         ≡⟨ ·-linv p ⟩
      refl a
    ∎

Moving a term from one side to the other is a common task, so let’s define a few handy functions for doing that.

·-left-to-right-l
  : ∀ {ℓ : Level} {A : Type ℓ} {a b c : A} {p : a ≡ b} {q : b ≡ c} {r : a ≡ c}
  → p · q ≡ r
  ------------------
  →     q ≡ ! p · r

·-left-to-right-l {a = a}{b = b}{c = c} {p} {q} {r} α =
  begin
    q
      ≡⟨ ·-lunit q ⟩
    refl b · q
      ≡⟨ ap (_· q) (! (·-linv p)) ⟩
    (! p · p) · q
      ≡⟨ ·-assoc (! p) p q ⟩
    ! p · (p · q)
      ≡⟨ ap (! p ·_) α ⟩
    ! p · r
  ∎

·-left-to-right-r
  : ∀ {ℓ : Level} {A : Type ℓ} {a b c : A} {p : a ≡ b} {q : b ≡ c} {r : a ≡ c}
  → p · q ≡ r
  -------------------
  →      p ≡ r · ! q

·-left-to-right-r {a = a}{b = b}{c = c} {p} {q} {r} α =
  begin
    p
      ≡⟨ ·-runit p ⟩
    p · refl b
      ≡⟨ ap (p ·_) (! (·-rinv q)) ⟩
    p · (q · ! q)
      ≡⟨ ! (·-assoc p q (! q)) ⟩
    (p · q) · ! q
      ≡⟨ ap (_· ! q) α ⟩
    r · ! q
  ∎

·-right-to-left-r
  : ∀ {ℓ : Level} {A : Type ℓ} {a b c : A} {p : a ≡ c} {q : a ≡ b} {r : b ≡ c}
  →       p ≡ q · r
  -------------------
  → p · ! r ≡ q

·-right-to-left-r {a = a}{b = b}{c = c} {p} {q} {r} α =
  begin
    p · ! r
      ≡⟨ ap (_· ! r) α ⟩
    (q · r) · ! r
      ≡⟨ ·-assoc q r (! r) ⟩
    q · (r · ! r)
      ≡⟨ ap (q ·_) (·-rinv r) ⟩
    q · refl b
      ≡⟨ ! (·-runit q) ⟩
    q
    ∎

·-right-to-left-l
  : ∀ {ℓ : Level} {A : Type ℓ} {a b c : A} {p : a ≡ c} {q : a ≡ b} {r : b ≡ c}
  →       p ≡ q · r
  ------------------
  → ! q · p ≡ r

·-right-to-left-l {a = a}{b = b}{c = c} {p} {q} {r} α =
  begin
    ! q · p
      ≡⟨ ap (! q ·_) α ⟩
    ! q · (q · r)
      ≡⟨ ! (·-assoc (! q) q r) ⟩
    ! q · q · r
      ≡⟨ ap (_· r) (·-linv q) ⟩
    refl b · r
      ≡⟨ ! (·-lunit r) ⟩
    r
  ∎

!-·
  : ∀ {ℓ : Level} {A : Type ℓ} {a b : A}
  → (p : a ≡ b)
  → (q : b ≡ a)
  --------------------------
  → ! (p · q) ≡ ! q · ! p

!-· idp q = ·-runit (! q)

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