Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-transformations.U
  where
  open import foundations.Core

  open import lib.graph-definitions.Graph
  open import lib.graph-homomorphisms.Hom
  open import lib.graph-homomorphisms.classes.Isomorphisms

  private
    variable
      ℓ : Level

  UEdge : (G : Graph ℓ) (x y : Node G) → Type ℓ
  UEdge G x y = (Edge G x y) + (Edge G y x)

  U : Graph ℓ → Graph ℓ
  U  g@(graph Ng Eg Ng-set Eg-set)
    = graph Ng
    (UEdge g)
    Ng-set
    λ x y → +-set (Eg-set x y) (Eg-set y x)

  U-reverse-edge
    : ∀ {ℓ : Level} {G : Graph ℓ} {x y : Node G}
    → Edge (U G) x y
    → Edge (U G) y x

  U-reverse-edge (inl xy) = inr xy
  U-reverse-edge (inr yx) = inl yx

  open import lib.graph-homomorphisms.Hom

  Hom-U : ∀ {ℓ₁ ℓ₂ : Level} {G : Graph ℓ₁}{H : Graph ℓ₂}
    → Hom G H
    → Hom G (U H)
  Hom-U h = hom (α h) λ x y e → inl (β h x y e)
    where open Hom

  open import lib.graph-classes.ConnectedGraph
  open import lib.graph-walks.Walk

  module _ {ℓ} {G : Graph ℓ} where
    walk-to-U-walk : ∀ {x y} → Walk G x y → Walk (U G) x y
    walk-to-U-walk ⟨ x ⟩ = ⟨ x ⟩
    walk-to-U-walk (e ⊙ w) = inl e ⊙ walk-to-U-walk w

    -- Lemma 5.4
    U-perserves-connectedness
      : G is-connected-graph
      → (U G) is-connected-graph
    U-perserves-connectedness G-is-cont x y
      = trunc-elim trunc-is-prop (λ w → ∣ walk-to-U-walk w ∣) (G-is-cont x y)

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