Investigations on graph-theoretical constructions in Homotopy type theory

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

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

  module _ {ℓ : Level}{G : Graph ℓ}
    where
    open import lib.graph-embeddings.Map
    open import lib.graph-embeddings.Map.Face
    open import lib.graph-embeddings.Map.Face.Walk.Homotopy

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

    module Whiskering (𝕄 : Map G)
      where

      open HomotopyWalks {G = G} 𝕄
      open ∙-walk (U G)

      whiskerR
        : ∀ {x y : Node G}
        → {xy₁ xy₂ : Walk (U G) x y}
        → xy₁ ∼⟨ 𝕄 ⟩∼ xy₂
        → ∀ {z : Node G} → (yz : Walk (U G) y z)
        → (xy₁ ∙w yz) ∼⟨ 𝕄 ⟩∼ (xy₂ ∙w yz)

      whiskerR {x}{y} (collapse F {a}{b} w₁ w₂) {z} yz
          = coe (! (ap² (_∼hwalk_ {x}{z})
            (∙w-assoc-four-walks w₁ _ w₂ yz)
            ((∙w-assoc-four-walks w₁ _ w₂ yz))))
            (collapse {x}{z} F {a} {b} w₁ (w₂ ∙w yz))
      whiskerR hwalk-refl yz = hwalk-refl
      whiskerR (hwalk-symm w) yz = hwalk-symm (whiskerR w yz)
      whiskerR (hwalk-trans {w₁}{w₂}{w₃} w₁∼w₂  w₂∼w₃) yz
          = hwalk-trans (whiskerR w₁∼w₂ yz) (whiskerR w₂∼w₃ yz)

      whiskerL
          : ∀ {x y : Node G}
          → (xy : Walk (U G) x y)
          → ∀ {z : Node G} → {yz₁ yz₂ : Walk (U G) y z}
          → yz₁ ∼⟨ 𝕄 ⟩∼ yz₂
          → (xy ∙w yz₁) ∼⟨ 𝕄 ⟩∼ (xy ∙w yz₂)

      whiskerL {x}{y} xy {z} {yz₁}{yz₂} (collapse F {a}{b} w₁ w₂)
           = coe ((ap² _∼hwalk_ (∙w-assoc xy w₁ _) (∙w-assoc xy w₁ _)))
           (collapse {x}{z} F {a}{b} (xy ∙w w₁) w₂)

      whiskerL _ hwalk-refl = hwalk-refl
      whiskerL xy (hwalk-symm w) = hwalk-symm (whiskerL xy w)
      whiskerL xy (hwalk-trans {w₁}{w₂}{w₃} w₁∼w₂ w₂∼w₃)
          = hwalk-trans (whiskerL xy w₁∼w₂) (whiskerL xy w₂∼w₃)

      whisker-h
          : ∀ {x y z : Node G}
          → {xy₁ xy₂ : Walk (U G) x y} {yz₁ yz₂ : Walk (U G) y z}
          → (xy₁ ∼⟨ 𝕄 ⟩∼ xy₂)
          → (yz₁ ∼⟨ 𝕄 ⟩∼ yz₂)
          -----------------------------------
          → (xy₁ ∙w yz₁) ∼⟨ 𝕄 ⟩∼ (xy₂ ∙w yz₂)

      whisker-h {x}{y}{z}{xy₁} {xy₂} {yz₁} {yz₂} H₁  H₂
          = hwalk-trans H-yz₁ H-yz₂
          where
          H-yz₁ : (xy₁ ∙w yz₁) ∼⟨ 𝕄 ⟩∼ (xy₂ ∙w yz₁)
          H-yz₁ = whiskerR H₁ yz₁

          H-yz₂ : (xy₂ ∙w yz₁) ∼⟨ 𝕄 ⟩∼ (xy₂ ∙w yz₂)
          H-yz₂ = whiskerL xy₂ H₂

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