Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-walks.Walk.Equality
  where
  open import foundations.Core
  open import lib.graph-definitions.Graph
  open import lib.graph-walks.Walk renaming (length to len)
  open Graph

  module _ {ℓ : Level} (G : Graph ℓ) where

    data _≅walk_ : ∀ {x y} → Walk G x y → Walk G x y → Type ℓ
      where
      dot : ∀ {x} → ⟨ x ⟩ ≅walk ⟨ x ⟩
      non-dot : ∀ {x y z} {w1 w2 : Walk G y z}
        → (e : Edge G x y) → w1 ≡ w2 → (e ⊙ w1) ≅walk (e ⊙ w2)

    ≅walk-refl : ∀ {x y} → {p : Walk G x y} → p ≅walk p
    ≅walk-refl {p = ⟨ _ ⟩} = dot
    ≅walk-refl {p = x ⊙ p} = non-dot x idp

    ≅walk-→-≡ : ∀ {x y} (w1 w2 : Walk G x y) → w1 ≅walk w2 → w1 ≡ w2
    ≅walk-→-≡ .(⟨ _ ⟩) .(⟨ _ ⟩) dot = idp
    ≅walk-→-≡ .(e ⊙ _) .(e ⊙ _) (non-dot e idp) = idp

    ≡-→-≅walk : ∀ {x y} (w1 w2 : Walk G x y) → w1 ≡ w2 → w1 ≅walk w2
    ≡-→-≅walk ⟨ _ ⟩ .(⟨ _ ⟩) idp = dot
    ≡-→-≅walk (e ⊙ w1) .(e ⊙ w1) idp = non-dot e idp

    ≡-≃-≅walk : ∀ {x y} (w1 w2 : Walk G x y) → (w1 ≡ w2) ≃ (w1 ≅walk w2)
    ≡-≃-≅walk ⟨ _ ⟩ w2
      = qinv-≃ (≡-→-≅walk ⟨ _ ⟩ w2)
               (≅walk-→-≡ _ w2 , (λ {dot → idp}) , λ {idp → idp})
    ≡-≃-≅walk w1@(e ⊙ p) ⟨ _ ⟩ = qinv-≃ (≡-→-≅walk w1 ⟨ _ ⟩) (≅walk-→-≡ w1 _ , (λ {()}) , λ {()})
    ≡-≃-≅walk (e ⊙ p) (e' ⊙ q)
      = qinv-≃ (≡-→-≅walk _ _)
               (≅walk-→-≡ _ _ , (λ {(non-dot .e idp) → 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