Cyclicgraphs excerpts

cubical.lagda.md

open import Cubical.Core.Everything
open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Data.Sum
open import Cubical.Data.Unit

record Graph {ℓ ℓ' : Level} (E : Type ℓ) (V : Type ℓ') : Type (ℓ-max ℓ ℓ') where
  field
    π₀ : E → V
    π₁ : E → V
open Graph {{...}}

data ⊥ (ℓ : Level) : Type ℓ where

record TGraph {ℓ : Level} (E : Type ℓ) (V : Type ℓ) : Type ℓ where
  field
    bar : E → E   -- inversion of an edge
    ι   : E → V   -- source
    -- rules
    bar-is-involution : (e : E) → bar (bar e) ≡ e
    bar-changes-first : (e : E) → (bar e) ≡ e → ⊥ ℓ
open TGraph {{...}}

module _  {ℓ : Level} {E V : Type ℓ}(Γ : TGraph E V) where
  source : E → V
  source e = TGraph.ι Γ e

  target : E → V
  target e = TGraph.ι Γ (TGraph.bar Γ e)

record TGraphMap {ℓ : Level} {E V : Type ℓ} (Γ : TGraph E V) {E' V' : Type ℓ} (Δ : TGraph E' V') : Type ℓ  where
  field
    edges-to-edges   : E → E'
    vertex-to-vertex : V → V'

data Coeq {ℓ ℓ' : Level} {V : Type ℓ} {E : Type ℓ'} (ev : Graph E V) :
          Type (ℓ-max ℓ ℓ')  where
  c[_] : V → (Coeq ev)
  quot : (e : E) → c[ (Graph.π₀ ev e) ] ≡ c[ (Graph.π₁ ev e) ]

_/_ : {ℓ ℓ' : Level} (V : Type ℓ) (E : Type ℓ') {{ ev : Graph E V }} →
         Type (ℓ-max ℓ ℓ')
_/_ V E {{ ev }} = Coeq ev
infix 25 _/_

module CoprodCoeq {ℓ ℓ' ℓ'' : Level} 
            (E₀ : Type ℓ) 
            (E₁ : Type ℓ') 
            (V : Type ℓ'')
            {{ ev : Graph (E₀ ⊎ E₁) V }} 
    where

  instance
    evE₀ : Graph E₀ V
    evE₀ = record { π₀ = π₀ ∘ inl ; π₁ = π₁ ∘ inl }

    ev-snd : Graph E₁ (V / E₀)
    ev-snd = record { π₀ = c[_] ∘ π₀ ∘ inr ; π₁ = c[_] ∘ π₁ ∘ inr }

  coeq-coprod-equiv : V / (E₀ ⊎ E₁) ≃ (V / E₀) / E₁
  coeq-coprod-equiv = isoToEquiv (iso f g f-g g-f)
    where
      f : V / (E₀ ⊎ E₁) → (V / E₀) / E₁
      f c[ x ] = c[ c[ x ] ]
      f (quot (inl e) i) = c[ quot e i ]
      f (quot (inr e) i) = quot e i

      g : (V / E₀) / E₁ →  V / (E₀ ⊎ E₁)
      g c[ c[ x ] ] = c[ x ]
      g c[ quot e i ] = quot (inl e) i
      g (quot e i) = quot (inr e) i

      f-g : (z : (V / E₀) / E₁) → (f (g z) ≡ z)
      f-g c[ c[ x ] ] = refl
      f-g c[ quot e i ] = refl
      f-g (quot e i) = refl

      g-f : (z : V / (E₀ ⊎ E₁)) → (g (f z) ≡ z)
      g-f c[ x ] = refl
      g-f (quot (inl e) i) = refl
      g-f (quot (inr e) i) = refl

module TrivialExtension {ℓ ℓ' : Level} (V : Type ℓ) (v : V) where
  instance
    evt-l : Graph Unit (V ⊎ Unit)
    evt-l = record { π₀ = λ x → inl v ; π₁ = inr }

    evt-r : Graph Unit (Unit ⊎ V)
    evt-r = record { π₀ = inl ; π₁ = λ _ → inr v }

  te-equiv-l : V ≃ (V ⊎ Unit) / Unit
  te-equiv-l = isoToEquiv (iso (c[_] ∘ inl) g f-g (λ _ → refl))
    where
      g : (V ⊎ Unit) / Unit → V
      g c[ inl x ] = x
      g c[ inr x ] = v
      g (quot e i) = v

      f-g : (z : (V ⊎ Unit) / Unit) → c[ inl (g z) ] ≡ z
      f-g c[ inl x ] = refl
      f-g c[ inr x ] = quot x
      f-g (quot e i) j = quot e (i ∧ j)

  te-equiv-r : V ≃ (Unit ⊎ V) / Unit
  te-equiv-r = isoToEquiv (iso (c[_] ∘ inr) g f-g λ _ → refl)
    where
      g : (Unit ⊎ V) / Unit → V
      g c[ inl x ] = v
      g c[ inr x ] = x
      g (quot e i) = v

      f-g : (z : (Unit ⊎ V) / Unit) → c[ inr (g z) ] ≡ z
      f-g c[ inl x ] i = quot x (~ i)
      f-g c[ inr x ] = refl
      f-g (quot e i) j = quot e (i ∨ ~ j)

Faces.lagda.md

title
On planarity of univalent graphs

{-# OPTIONS --without-K --exact-split --allow-unsolved-metas --rewriting #-}

module lib.graph-families.CycleGraph.Faces
  where
  open import foundations.Core
  open import lib.graph-definitions.Graph
  open Graph
  module
    _ (ℓ : Level)
    where
    open import lib.graph-classes.CyclicGraph
    open import lib.graph-families.CycleGraph ℓ
    open import lib.graph-families.CycleGraph.RotHom ℓ

    open import foundations.Nat ℓ

    module _ (n : ℕ) (n>0 : n > 0) where

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

      𝕄 : Map (Cycle n)
      𝕄 = Cn-Map₁ ℓ n
        where
        open import lib.graph-families.CycleGraph.Map

      open import lib.graph-families.CycleGraph.isCyclicGraph

      -- F₁ will correspond to the inner face in Cn.
      F₁ : Face (Cycle n) 𝕄
      Face.A F₁ = Cycle n
      Face.A↺ F₁ = Cn-is-cyclic-graph ℓ n
      Face.one-point-at-least F₁ = n>0
      Face.h F₁ = hom id λ x y e → inl e
        where open import lib.graph-homomorphisms.Hom
      Face.h-is-edge-inj F₁ = λ {e₁ e₂ idp → idp}
      Face.edge-order-preservation F₁ = {!!}

      open import lib.graph-transformations.Inv

      postulate
        F₂ : Face (Cycle n) 𝕄

      -- Face.A F₂ = Cycle n
      -- Face.A↺ F₂ = Cn-is-cyclic-graph ℓ n
      -- Face.one-point-at-least F₂ = n>0
      -- Face.h F₂ ={!   !}}
      -- Face.h-is-edge-inj F₂ ={!   !}}
      -- Face.edge-order-preservation F₂ ={!   !}}

isPlanar.lagda.md

title
On planarity of univalent graphs

{-# OPTIONS --without-K --exact-split --rewriting --allow-unsolved-metas #-}

module lib.graph-families.CycleGraph.isPlanar
  where
  open import foundations.Core
  open import lib.graph-definitions.Graph
  open Graph

  module
    _
    (ℓ : Level)
    where

    open import foundations.Nat ℓ
    open import foundations.Fin ℓ
    open import lib.graph-families.CycleGraph ℓ
    open import lib.graph-embeddings.Map
    open import lib.graph-transformations.U

    open import lib.graph-families.CycleGraph.Map
    open import lib.graph-families.CycleGraph.isCyclicGraph
    open import lib.graph-families.CycleGraph.Walk

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

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

    open import lib.graph-embeddings.Map.Spherical

    module _ (n : ℕ) (n>0 : n > 0) where

      open simplewalks
      open import lib.graph-families.CycleGraph.isFiniteGraph

      UCn-is-connected :  isConnectedGraph (U (Cycle n))
      UCn-is-connected x y = ∣ ccw _ n x y ∣

      postulate
        Cn-Map-is-spherical : isSphericalMap (Cycle n) (Cn-Map₁ _ n)

      open import lib.graph-families.CycleGraph.Faces using (F₁ ; F₂)
      open import lib.graph-embeddings.Planar
      Cn-is-planar : Planar (Cycle n)
      Cn-is-planar = UCn-is-connected , (Cn-Map₁ _ n , Cn-Map-is-spherical  , F₁ _ n n>0)