Investigations on graph-theoretical constructions in Homotopy type theory

  module _ {ℓ : Level} 
    (G : Graph ℓ)
    (_≟Node_ : (x y : Node (U G)) → (x ≡ y) + (x ≠ y))
    (M : Map G)
    (M-is-spherical : isSphericalMap G M)
    where

The following is a proof of Lemma 1.1. § 2.3 in Testing Homotopy for Paths in the Plane by Cabello, Sergio Liu, Yuanxin Mantler, Andrea Snoeyink, Jack. Springer.

Lemma: Two paths have the same canonical sequence if and only if they are homotopic (in the plane).

We replace cannonical by normal form in the sense of our loop-reduction relation.

    
    open lib.graph-embeddings.HIT.construction G M
    [_]ₕᵢₜ = to-eq 𝕟 𝕖 

    variable
      x y : Node G
    
    lemma
      : (p q : Walk (U G) x y) 
      → p ∼⟨ M ⟩∼ q
      -------------------------
      → ∥ [ p ]ₕᵢₜ ≡ [ q ]ₕᵢₜ ∥ 

    lemma _ _ (hwalk-refl) = ∣ idp ∣ 
    lemma _ _ (hwalk-symm q∼p) 
      = trunc-elim trunc-is-prop (λ q=p → ∣ ! q=p ∣ ) (lemma _ _ q∼p)
    lemma _ _ (hwalk-trans {w₂ = w₂} p∼w₂ w₂∼q)
      = trunc-elim trunc-is-prop (λ p=w₂
      → trunc-elim trunc-is-prop (λ w₂=q → ∣ p=w₂ · w₂=q ∣) ∣w₂=q∣) ∣p=w₂∣ 
      where
      ∣p=w₂∣ = lemma _ w₂ p∼w₂
      ∣w₂=q∣ = lemma w₂ _ w₂∼q
    lemma _ _  (collapse 𝔽 {a}{b} w₁ w₂) = ∣ helper ∣
      where
      helper = 
        begin
          [ w₁ ·w (cw-walk _ {M} 𝔽 a b ∙w w₂) ]ₕᵢₜ                ≡⟨ i ⟩ 
          [ w₁ ]ₕᵢₜ · [ cw-walk _ {M} 𝔽 _ _ ∙w w₂ ]ₕᵢₜ            ≡⟨ ii ⟩ 
          [ w₁ ]ₕᵢₜ · ([ cw-walk _ {M} 𝔽 _ _  ]ₕᵢₜ · [ w₂ ]ₕᵢₜ)   ≡⟨ iii ⟩ 
          [ w₁ ]ₕᵢₜ · ([ ccw-walk _ {M} 𝔽 _ _  ]ₕᵢₜ · [ w₂ ]ₕᵢₜ)  ≡⟨ iv ⟩ 
          [ w₁ ]ₕᵢₜ · [ ccw-walk _ {M} 𝔽 _ _ ∙w w₂ ]ₕᵢₜ           ≡⟨ v ⟩ 
          [ w₁ ·w ccw-walk _ {M} 𝔽 a b ∙w w₂ ]ₕᵢₜ                 ∎
        where
        i  = to-eq-compatible-·w  𝕟 𝕖 w₁ (cw-walk _ {M} 𝔽 a b ∙w w₂) 
        ii  = ap ([ w₁ ]ₕᵢₜ ·_) (to-eq-compatible-·w  𝕟 𝕖 (cw-walk _ {M} 𝔽 a b) w₂)
        iii = ap ([ w₁ ]ₕᵢₜ ·_)  (ap (_· [ w₂ ]ₕᵢₜ) (𝕗 𝔽 a b)) 
        iv  = ap (λ o → [ w₁ ]ₕᵢₜ · o) (! to-eq-compatible-·w 𝕟 𝕖 (ccw-walk _ {M} 𝔽 a b) w₂)
        v   = ! to-eq-compatible-·w 𝕟 𝕖 w₁ ((ccw-walk _ {M} 𝔽 a b ∙w w₂))

    -- -- Note that the following holds because we have a spherical map.
    corollary
      :  ∀ {x y : Node G}
      → (p q : Walk (U G) x y) 
      → ∥ [ p ]ₕᵢₜ ≡ [ q ]ₕᵢₜ ∥ 
    corollary p q  = trunc-elim trunc-is-prop (λ p∼q → lemma _ _ p∼q) ∣p∼q∣
        where
        ∣p∼q∣ : ∥ p ∼⟨ M ⟩∼ q ∥
        ∣p∼q∣ = lemap (spherical-equiv G (_≟Node_) M) M-is-spherical _ _ p 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