lib.graph-embeddings.Map.Face.Example.md.

Version of Sunday, January 22, 2023, 10:42 PM

Powered by agda version 2.6.2.2-442c76b and pandoc 2.14.0.3

Investigations on graph-theoretical constructions in Homotopy type theory

Jonathan Prieto-Cubides j.w.w. HΓ₯kon Robbestad Gylterud

Department of Informatics

University of Bergen, Norway

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

module lib.graph-embeddings.Map.Face.Example
  where
  open import foundations.Core
  open import lib.graph-definitions.Graph
  open import lib.graph-transformations.U
  open Graph

  open import lib.graph-embeddings.Map
  open import lib.graph-classes.UnitGraph

  open import foundations.Cyclic using (CyclicSet; cyclic-set)
  open import foundations.Fin
  open import foundations.Nat


  open import lib.graph-embeddings.Map
  open import lib.graph-definitions.Graph
  open import lib.graph-homomorphisms.Hom
  open import lib.graph-homomorphisms.classes.EdgeInjective
  open import lib.graph-transformations.U
  open import lib.graph-classes.CyclicGraph
  open import lib.graph-classes.CyclicGraph.Stuff
  open import lib.graph-embeddings.Map.Face

  open import lib.graph-embeddings.Planar
  open import lib.graph-classes.EmptyGraph
  empty-is-planar : Planar (𝟘-graph lzero)
  empty-is-planar = Ξ» {()}

  β„“ : Level
  β„“ = lzero
  β—Ž = πŸ™-graph lzero

  open import foundations.Fin
  open import lib.graph-classes.UnitGraph
  open import lib.graph-classes.EmptyGraph
  open import foundations.Cyclic
  open import foundations.UnivalenceAxiom
  open CyclicSet-is-set
  open import lib.graph-classes.CyclicGraph
  open CyclicGraph-is-set

  star-πŸ™ : (Star (πŸ™-graph β„“) βˆ— ≃ Fin β„“ 0)
  star-πŸ™ = qinv-≃ (Ξ» { (_ , inl ()) ; (_ , inr ())})
                    ((Ξ» { (zero , ()) ; (succ _ , ())}) ,
                    (Ξ» { (zero , ()) ; (succ _ , ())}) , Ξ» { (_ , inl ()) ; (_ , inr ())})


  zero-is-only-once-cyclic : isProp (CyclicSet β„“ (Fin β„“ 0))
  zero-is-only-once-cyclic p q = rapply (lemma-2-13 β„“ {A = Fin β„“ 0} p q)
      (pi-is-prop (Ξ» _ β†’ isProp-≃ (𝟘-≃-⟦0⟧ β„“) 𝟘-is-prop) _ _)

  πŸ™-map : Map (πŸ™-graph β„“ )
  πŸ™-map βˆ— = cyclic-set id 0 ∣ star-πŸ™ , funext (Ξ» { (fst₁ , inl ()) ; (fst₁ , inr ())}) ∣
    where
    open import foundations.FunExtAxiom

  πŸ™-has-prop-map : isProp (Map (πŸ™-graph β„“))
  πŸ™-has-prop-map = (pi-is-prop (Ξ» {* β†’ tr (Ξ» o β†’ isProp (CyclicSet β„“ o)) (! ua star-πŸ™)
                         zero-is-only-once-cyclic}))

  πŸ™-graph-is-cyclic : CyclicGraph β„“ (πŸ™-graph β„“)
  πŸ™-graph-is-cyclic = cyclic-graph (id-hom (πŸ™-graph β„“)) 0 ∣ idp ∣

  πŸ™-hom : Hom (πŸ™-graph β„“) (U (πŸ™-graph β„“))
  πŸ™-hom = hom id (Ξ» _ _ abs β†’ inl abs)

  πŸ™-hom-prop' : isProp (Hom (πŸ™-graph β„“) (πŸ™-graph β„“))
  πŸ™-hom-prop' = isProp-≃ (≃-sym (Hom-≃-βˆ‘ (πŸ™-graph β„“) (πŸ™-graph β„“)))
    (βˆ‘-prop (pi-is-prop (Ξ» _ β†’ πŸ™-is-prop))
      (Ξ» {_ β†’ pi-is-prop
      (Ξ» _ β†’ pi-is-prop (Ξ» _ β†’ pi-is-prop
      (Ξ» _ β†’ 𝟘-is-prop )))}))

  πŸ™-hom-prop : isProp (Hom (πŸ™-graph β„“) (U (πŸ™-graph β„“)))
  πŸ™-hom-prop = isProp-≃ (≃-sym (Hom-≃-βˆ‘ (πŸ™-graph β„“) (U (πŸ™-graph β„“))))
      (βˆ‘-prop (pi-is-prop (Ξ» _ β†’ πŸ™-is-prop))
       (Ξ» {_ β†’ pi-is-prop
       (Ξ» _ β†’ pi-is-prop (Ξ» _ β†’ pi-is-prop
       (Ξ» _ β†’ +-prop 𝟘-is-prop 𝟘-is-prop (Ξ» {()}))))}))

  πŸ™-graph-cyclic-prop : isProp (CyclicGraph β„“ (πŸ™-graph β„“))
  πŸ™-graph-cyclic-prop = isProp-≃ CyclicGraph-≃-βˆ‘s
      (βˆ‘-prop πŸ™-hom-prop' Ξ» {_ (n , c) (m , d)
        β†’ pair= (instances-have-same-natural β„“ (πŸ™-graph β„“)
            (cyclic-graph  _ n c)
            (cyclic-graph  _ m d)
                , trunc-is-prop _ d) })

  πŸ™-face : Face (πŸ™-graph β„“) πŸ™-map
  πŸ™-face = face (πŸ™-graph β„“) πŸ™-graph-is-cyclic  πŸ™-hom
                        (Ξ» {()}) (Ξ» _ β†’ id)  (Ξ» {_ _ ()})

  helper : βˆ€ {A : Graph β„“}
         β†’ isProp (Hom A (U (πŸ™-graph β„“)))
  helper {A} = isProp-≃ ( ≃-sym (Hom-≃-βˆ‘ A _))
                 (βˆ‘-prop (pi-is-prop Ξ» _ β†’ πŸ™-is-prop)
                   Ξ» _ β†’ pi-is-prop (Ξ» _ β†’ pi-is-prop (Ξ» _
                     β†’ pi-is-prop (Ξ» _ β†’ +-prop 𝟘-is-prop 𝟘-is-prop (Ξ» {()})))))

  open import lib.graph-relations.Isomorphic

  UπŸ™-β‰…-πŸ™ : U (πŸ™-graph β„“) β‰… πŸ™-graph β„“
  UπŸ™-β‰…-πŸ™ = idEqv , Ξ» _ _ β†’ prop-ext-≃ (+-prop 𝟘-is-prop 𝟘-is-prop (Ξ» {()})) 𝟘-is-prop
    ((Ξ» { (inl ()) ; (inr ())}) , Ξ» {()})

  -- TODO: FIX the lemmas below:
  -- hom-implies-equals-to-πŸ™
  --   : (A : Graph β„“) β†’ Hom A (U (πŸ™-graph β„“)) β†’ A β‰… U (πŸ™-graph β„“)
  -- hom-implies-equals-to-πŸ™ A (hom Ξ± Ξ²)
  --   = {!!} , {!Ξ±!}


  -- πŸ™-face-data-is-prop : isProp (faceData (πŸ™-graph β„“) πŸ™-map)
  -- πŸ™-face-data-is-prop (a , c , f) (b , d , g)
  --   = {!!}

  -- πŸ™-has-at-most-one-face : isProp (Face' (πŸ™-graph β„“) πŸ™-map)
  -- πŸ™-has-at-most-one-face
  --   = βˆ‘-prop πŸ™-face-data-is-prop
  --            (Ξ» d β†’ faceCond-is-prop {β„“} (πŸ™-graph β„“) {πŸ™-map} d)


  open import lib.graph-embeddings.Map.Face.Walk.Homotopy
  open HomotopyWalks
  open import lib.graph-embeddings.Map.Spherical
  open import lib.graph-walks.Walk

  M-is-spherical : isSphericalMap β—Ž πŸ™-map
  M-is-spherical βˆ— .βˆ— ⟨ .βˆ— ⟩ ⟨ .βˆ— ⟩ _ _ = ∣ hwalk-refl ∣
  M-is-spherical x .x ⟨ .x ⟩ (inl e βŠ™ w) = 𝟘-elim e
  M-is-spherical x .x ⟨ .x ⟩ (inr e βŠ™ w) = 𝟘-elim e
  M-is-spherical x y (inl e βŠ™ w1) w2 = 𝟘-elim e
  M-is-spherical x y (inr e βŠ™ w1) w2 = 𝟘-elim e

  open import lib.graph-classes.ConnectedGraph
  β—Ž-is-connected : (U β—Ž) is-connected-graph
  β—Ž-is-connected βˆ— βˆ— = ∣ ⟨ βˆ— ⟩ ∣

  β—Ž-is-planar : Planar β—Ž
  β—Ž-is-planar = Ξ» _ β†’ β—Ž-is-connected , πŸ™-map , M-is-spherical , πŸ™-face

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