Investigations on graph-theoretical constructions in Homotopy type theory

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


module lib.graph-embeddings.Map.Face.Walk.Homotopy
  where
  open import foundations.Core
  open import lib.graph-definitions.Graph
  open Graph
  open import lib.graph-homomorphisms.Hom

  open import lib.graph-embeddings.Map
  open import lib.graph-transformations.U

  module HomotopyWalks {ℓ : Level} {G : Graph ℓ}  (𝕄 : Map G)
    where

    open import lib.graph-walks.Walk
    open import lib.graph-walks.Walk.Composition

    open import lib.graph-embeddings.Map.Face
    open import lib.graph-embeddings.Map.Face.Walk

    open FaceWalks {ℓ} G
    open ∙-walk (U G)

    data
      _∼hwalk_
        {x y : Node (U G)}
        : Walk (U G) x y
        → Walk (U G) x y
        → Type (lsuc ℓ)
      where
      -- Equiv. Relation:
      hwalk-refl
        : ∀ {w₁ : Walk (U G) x y}
        → ---------
        w₁ ∼hwalk w₁

      hwalk-symm
        : ∀ {w₁ w₂ : Walk (U G) x y}
        → w₁ ∼hwalk w₂
        -------------
        → w₂ ∼hwalk w₁

      hwalk-trans
        : ∀ {w₁ w₂ w₃ : Walk (U G) x y}
        → w₁ ∼hwalk w₂ → w₂ ∼hwalk w₃
        ------------------------------
        → w₁ ∼hwalk w₃

      -- Deforming along a face.
      collapse
        : (𝔽 : Face G 𝕄) → {a b : Node (Face.A 𝔽)}
        → (w₁ : Walk (U G) x (Hom.α (Face.h 𝔽) a))
        → (w₂ : Walk (U G) (Hom.α (Face.h 𝔽) b) y)
        → (w₁ ·w (cw-walk 𝔽 a b) ∙w w₂) ∼hwalk (w₁ ·w (ccw-walk 𝔽 a b) ∙w w₂)

  HomotopyFace = HomotopyWalks._∼hwalk_
  syntax HomotopyFace map w1 w2 = w1 ∼⟨ map ⟩∼ w2

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