lib.graph-classes.UnitGraph.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-classes.UnitGraph
  where
  open import foundations.Core
  open import foundations.Fin
  open import foundations.Nat

  open import lib.graph-definitions.Graph
  open Graph

  πŸ™-graph : βˆ€ (β„“ : Level) β†’ Graph β„“
  πŸ™-graph β„“ = graph (πŸ™ β„“) (Ξ» _ _ β†’ (𝟘 β„“))
                    (prop-is-set πŸ™-is-prop)
                      \_ _  β†’ 𝟘-is-set

  open import lib.graph-relations.Isomorphic
  open import lib.graph-homomorphisms.classes.Isomorphisms
  open import lib.graph-homomorphisms.Hom

  only-one-iso : {β„“ : Level} β†’ (Aut (πŸ™-graph β„“)) ≃ πŸ™ β„“
  only-one-iso {β„“} = qinv-≃ (Ξ» _ β†’ βˆ—) ((Ξ» _ β†’ is-iso-to-β‰… ( id-hom (πŸ™-graph β„“) ) (id-iso (πŸ™-graph β„“)))
    , (Ξ» { βˆ— β†’ idp}) , Ξ» {(Ξ± , Ξ²) -- FIX: make it nicer.
      β†’ pair= (βˆ‘-prop (pi-is-prop (Ξ» _ β†’ πŸ™-is-prop)) is-equiv-is-prop _ _
              , pi-is-prop (Ξ» { βˆ— β†’ pi-is-prop (Ξ» { βˆ— β†’ equiv-iff-hprop 𝟘-is-prop 𝟘-is-prop})})
              _ _)})

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