lib.graph-walks.Walk.SigmaWalks.md.

Version of Sunday, January 22, 2023, 10:42 PM

Powered by agda version 2.6.2.2-442c76b and pandoc 2.14.0.3


Investigations on graph-theoretical constructions in Homotopy type theory

Jonathan Prieto-Cubides j.w.w. Håkon Robbestad Gylterud

Department of Informatics

University of Bergen, Norway

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

module lib.graph-walks.Walk.SigmaWalks
  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
    Walk-∑ :   Node G  Node G   Type 
    Walk-∑ 0 x y = x  y
    Walk-∑ (succ n) a c = ∑[ b ] (Edge G a b) × Walk-∑ n b c

    to-∑ :  {x y}  Walk G x y  ∑[ n ] Walk-∑ n x y
    to-∑  x    = (0 , idp)
    to-∑ (e  w) with (to-∑ w)
    ... | (n , q) = succ n , _ , e , q

    from-∑ :  {x y}  ∑[ n ] Walk-∑ n x y   Walk G x y
    from-∑ (zero , idp) =  _ 
    from-∑ (succ n , (b , (e , w))) = e  from-∑ (n , w)

    Walk-is-equiv-to-Walk-∑ :   {x y}  Walk G x y  (∑[ n ] Walk-∑ n x y)
    Walk-is-equiv-to-Walk-∑ = qinv-≃ to-∑ (from-∑ , h1 , h2)
      where
      h1 :  {x y}  (q : ∑[ n ] Walk-∑ n x y)  to-∑ (from-∑ q)  q
      h1 (zero , idp) = idp
      h1 (succ n , (b , (e , w))) with to-∑ (from-∑ (n , w)) | h1 (n ,  w)
      ... | .n , .w | idp = idp

      h2 :  {x y}  (w : Walk G x y)  from-∑ (to-∑ w)  w
      h2  _  = idp
      h2 (e  w) = ap (e ⊙_) (h2 w)

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