Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-classes.CyclicGraph.Walk
  where
  open import foundations.Core
  open import lib.graph-definitions.Graph
  open import lib.graph-homomorphisms.Hom
  open import lib.graph-homomorphisms.classes.Isomorphisms
  open import lib.graph-relations.Isomorphic
  open import lib.graph-classes.UndirectedGraph
  open import lib.graph-embeddings.Map

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

  open import lib.graph-classes.CyclicGraph.Stuff

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

    module
      UndirectedWalks
      where
        
      -- NOTE: when a = b, we want this to be ⟨ a ⟩
      ccw-walk
          : (G-cyclic : CyclicGraph ℓ G)
          → (a b : Node G)
          ----------------
          → Walk (U G) a b

      ccw-walk G-cyclic@(cyclic-graph f zero c)     a b
        = tr (λ o → Walk (U G) a o)
          (trunc-elim (Node-is-set G _ _)
            (λ {idp → 𝟙-is-prop _ _})
            c)
          ⟨ a ⟩
      ccw-walk G-cyclic@(cyclic-graph f (succ n) c) a b = walk
        where
        open cyclic-graph-stuff G G-cyclic
        open import lib.graph-families.CycleGraph

        steps : ∑[ k ] ((pred-↺ ^ (π₁ k)) a ≡ b) × _
        steps = ccw-node-steps G G-cyclic a b

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

        ccw-walk'
            : (c : Node G)
            → (k : ℕ)
            → Walk (U G) c ((pred-↺ ^ k) c)

        ccw-walk' c zero = ⟨ c ⟩
        ccw-walk' c (succ n)
          = tr (Walk (U G) c) (! (app-comm pred-↺ n c))
            (inr (pred-edge G G-cyclic ∗ c) ⊙ ccw-walk' (pred-↺ c) n)

        walk : Walk (U G) a b
        walk = tr (Walk (U G) a) (π₁ (π₂ steps)) (ccw-walk' a k)


      cw-walk
          : (G-cyclic : CyclicGraph ℓ G)
          → (a b : Node G)
          ----------------
          → Walk (U G) a b

      cw-walk G-cyclic@(cyclic-graph f zero c) a b
        = tr (λ o → Walk (U G) a o)
          (trunc-elim (Node-is-set G _ _)
            (λ {idp → 𝟙-is-prop _ _})
            c)
          ⟨ a ⟩

      cw-walk G-cyclic@(cyclic-graph f (succ n) c) a b = walk
        where
        open cyclic-graph-stuff G G-cyclic
        steps : ∑[ k ] ((suc-↺ ^ (π₁ k)) a ≡ b) × _
        steps = (cw-node-steps G G-cyclic a) b

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

        cw-walk'
          : (c : Node G)
          → (k : ℕ)
          → Walk (U G) (c) (((suc-↺ ^ k) c))

        cw-walk' c zero = ⟨ c ⟩
        cw-walk' c (succ n)
          = tr (Walk (U G) c) (! (app-comm suc-↺ n c))
            (inl (suc-edge G G-cyclic unit c) ⊙ cw-walk' (suc-↺ c) n)

        walk : Walk (U G) a b
        walk = tr (Walk (U G) a) (π₁ (π₂ 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