Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-embeddings.Map.Face.Walk
  where
  open import foundations.Core
  open import lib.graph-embeddings.Map
  open import lib.graph-embeddings.Map.Face

  open import lib.graph-definitions.Graph
  open Graph

  open import lib.graph-walks.Walk
  open import lib.graph-transformations.U

  open import lib.graph-homomorphisms.Hom

  open import lib.graph-classes.CyclicGraph.Stuff

  module
    FaceWalks
    {ℓ : Level}
    (G : Graph ℓ)
    where
    open import lib.graph-classes.CyclicGraph
    ccw-walk
        : {𝕄 : Map G}
        → (𝔽 : Face G 𝕄)
        → (a b : Node (Face.A 𝔽))
        ----------------
        → Walk (U G) (Hom.α (Face.h 𝔽) a) (Hom.α (Face.h 𝔽) b)

    -- NOTE: review everything to check it follows our intuition:
    -- If a = b, then ccw(a,b) = ⟨ a ⟩ and cw(a,b) = e₁⋯eₖ.
    ccw-walk 𝔽@(face A A↺@(cyclic-graph φ zero c) h p₁ p₂ p₃) a b
      = tr (λ o → Walk (U G) (Hom.α (Face.h 𝔽) a) (Hom.α (Face.h 𝔽) o))
           (trunc-elim (Node-is-set A _ _)
             (λ {idp → 𝟙-is-prop _ _})
             c)
           ⟨ Hom.α h a ⟩

    ccw-walk 𝔽@(face A A↺@(cyclic-graph φ (succ n) c) h p₁ p₂ p₃) a b = walk
      where
      open cyclic-graph-stuff A A↺
      steps : ∑[ k ] ((pred-↺ ^ (π₁ k)) a ≡ b) × _
      steps = ccw-node-steps A A↺ a b
      k : ℕ
      k = π₁ (π₁ steps)

      ccw-walk'
          : (c : Node A)
          → (k : ℕ)
          → Walk (U G) (Hom.α h c) (Hom.α h ((pred-↺ ^ k) c))
      ccw-walk' c zero = ⟨ Hom.α h c ⟩
      ccw-walk' c (succ n)
        = tr (Walk (U G) (Hom.α h c)) (ap (Hom.α h) (! (app-comm pred-↺ n c)))
          (π₂ (edge-in-star-with-pred A↺ h unit c) ⊙ ccw-walk' (pred-↺ c) n)

      walk : Walk (U G) (Hom.α h a) (Hom.α h b)
      walk = tr (λ x → Walk (U G) (Hom.α h a) (Hom.α h x))
                (π₁ (π₂ steps)) (ccw-walk' a k)
    cw-walk
        : {𝕄 : Map G}
        → (𝔽 : Face G 𝕄)
        → (a b : Node (Face.A 𝔽))
        ----------------
        → Walk (U G) (Hom.α (Face.h 𝔽) a) (Hom.α (Face.h 𝔽) b)

    cw-walk 𝔽@(face A A↺@(cyclic-graph φ zero c) h p₁ p₂ p₃) a b
      = tr (λ o → Walk (U G) (Hom.α (Face.h 𝔽) a) (Hom.α (Face.h 𝔽) o))
           (trunc-elim (Node-is-set A _ _)
             (λ {idp → 𝟙-is-prop _ _})
             c)
           ⟨ Hom.α h a ⟩
    cw-walk 𝔽@(face A A↺@(cyclic-graph φ (succ n) c) h p₁ p₂ p₃) a b  = walk
      where

      open cyclic-graph-stuff A A↺
      steps : ∑[ k ] ((suc-↺ ^ (π₁ k)) a ≡ b) × _
      steps = cw-node-steps A A↺ a b

      k : ℕ
      k = π₁ (π₁ steps)

      cw-walk'
        : (c : Node A)
        → (k : ℕ)
        → Walk (U G) (Hom.α (Face.h 𝔽) c) (Hom.α (Face.h 𝔽) ((suc-↺ ^ k) c))

      cw-walk' c zero = ⟨ Hom.α (Face.h 𝔽) c ⟩
      cw-walk' c (succ n)
        = tr (Walk (U G) (Hom.α (Face.h 𝔽) c)) (ap (Hom.α (Face.h 𝔽)) (! (app-comm suc-↺ n c)))
        (ge.suc-edge-from  (Face.A↺ 𝔽) (Face.h 𝔽) unit c  ⊙ cw-walk' (suc-↺ c) n)

      walk : Walk (U G) (Hom.α (Face.h 𝔽) a) (Hom.α (Face.h 𝔽) b)
      walk = tr (λ x → Walk (U G) (Hom.α (Face.h 𝔽) a) (Hom.α (Face.h 𝔽) x)) (π₁ (π₂ steps)) (cw-walk' a k)

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