Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-embeddings.Map
  where
  open import foundations.Core

  open import lib.graph-definitions.Graph
  open Graph
  open import lib.graph-transformations.U

  Star : ∀ {ℓ : Level} (G : Graph ℓ) → Node G → Type ℓ
  Star G x = ∑[ y ∶ Node (U G) ] Edge (U G) x y

  Map : ∀ {ℓ : Level}(G : Graph ℓ) → Type ℓ
  Map {ℓ} G = Π[ x ∶ Node G ] CyclicSet (Star G x)
    where
    open import foundations.Cyclic ℓ

  --  Other names found in the literature:
  CombinatorialEmbedding = Map
  RotationSystem         = Map
  CellularEmbedding      = Map
  CombinatorialSurface   = Map

  module _ {ℓ : Level} (G : Graph ℓ) where
    Star-is-set : (x : Node G) → isSet (Star G x)
    Star-is-set x = ∑-set (Node-is-set (U G)) λ _ → Edge-is-set (U G) _ _

    Map-is-set : isSet (Map G)
    Map-is-set = pi-is-set (λ x → CyclicSet-is-set.proof {A = Star G x} )
      where open import foundations.Cyclic ℓ

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