Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-walks.Walk
  where
  open import foundations.Core

  open import lib.graph-definitions.Graph
  open Graph

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

    private
      variable
        x y z : Node G

    data
      Walk
        : Node G → Node G → Type ℓ
      where
      ⟨_⟩ : (x : Node G) → Walk x x
      _⊙_ : Edge G x y → Walk y z
          → Walk x z

    data Walk' : Node G → Node G → Type ℓ
      where
      ⟨_⟩' : (x : Node G) → Walk' x x
      _⊙'_ :  Walk' x y →  Edge G y z → Walk' x z

    length : ∀ {x y : Node G} → Walk x y → ℕ
    length ⟨ _ ⟩   = 
    length (x ⊙ w) = succ (length w)
    
    elim-principle
      : (P : ∀ {x z} → Walk x z → Type ℓ)
      → ((x : Node G) → P ⟨ x ⟩)
      → (∀ {x z} → (y : Node G)(e : Edge G x y) (w : Walk y z)
          → P w → P (e ⊙ w))
      → (∀ x y → (w : Walk x y) → P w)
    elim-principle P trivial composite _ _ ⟨ _ ⟩ = trivial _
    elim-principle P trivial composite _ _ (x ⊙ w) 
      = composite _ x w (elim-principle P trivial composite _ _ w)

    module _ {x y : Node G} where

      start-of : Walk x y → Node G
      start-of _ = x

      end-of : Walk x y → Node G
      end-of _ = y

The following notion of membership in a walk for a point is a bit different from the usual.

  module
    ∈-walk
      {ℓ : Level}
      (G : Graph ℓ)
    where

    private
      variable
        x y z : Node G

    _∈w_ : Node G → Walk G x z → Type ℓ
    y ∈w ⟨ z ⟩   = ⊥ ℓ
    y ∈w (e ⊙ w) = (y ≡ source G e) + (y ∈w 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