lib.graph-embeddings.Map.Face.isSet.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.isSet
  where
  open import foundations.Core
  open import foundations.HLevelLemmas

  open import foundations.NaturalsType
  open import foundations.Nat

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

  open import lib.graph-definitions.Graph
  open Graph

  open import lib.graph-walks.Walk
  open import lib.graph-transformations.U

  open import lib.graph-homomorphisms.Hom
  open Hom

  open import lib.graph-classes.CyclicGraph
  open CyclicGraph
  open import lib.graph-classes.CyclicGraph.Stuff

  open import lib.graph-homomorphisms.classes.EdgeInjective

  module _
    {β„“ : Level} (G : Graph β„“) (𝕄 : Map G)
    where

    abstract
      Face'-is-set : isSet (Face' G 𝕄)
      Face'-is-set f1@(d1@(A , Aβ†Ί@(cyclic-graph Ο†A zero pA) , f) , (p₁ , pβ‚‚) , p₃)
                  f2@(d2@(B , Bβ†Ί@(cyclic-graph Ο†B zero pB) , g) , (q₁ , qβ‚‚) , q₃)
        =  trunc-elim prop-is-prop (Ξ» {idp β†’ trunc-elim prop-is-prop
                      (Ξ» {idp β†’ isProp-≃ (≃-sym (≃-trans (Face'-Path-space G 𝕄 f1 f2) equiv))
                           (βˆ‘-prop (βˆ‘-prop (equiv-preserves-prop
                                      (≃-sym (≃-trans equiv-principle only-one-iso)) πŸ™-is-prop)
                                        (Ξ» {_ β†’ Hom-is-set _ _ _ _}))

                             (Ξ» _ β†’ Hom-is-set A B _ _))
                           }) pB}) pA
       where
       open import lib.graph-classes.UnitGraph
       open import lib.graph-definitions.Graph.EquivalencePrinciple
       open EquivPrinciple (πŸ™-graph β„“) (πŸ™-graph β„“)
       equiv : (d1 ≑ d2) ≃ (βˆ‘[ p ∢ βˆ‘[ Ξ± ∢ A ≑ B ] (tr _ Ξ± f ≑ g)  ] ((tr _ (π₁ p) Ο†A) ≑ Ο†B))
       equiv = begin≃
              _
               β‰ƒβŸ¨ qinv-≃ (Ξ» {idp β†’ idp}) ((Ξ» {idp β†’ idp}) , (Ξ» {idp β†’ idp}) , (Ξ» {idp β†’ idp})) ⟩
              Path {A = βˆ‘[ _ ] βˆ‘[ _ ] βˆ‘[ _ ]  _ }
              (A , f , Ο†A , pA)
              (B , g , Ο†B , pB)
               β‰ƒβŸ¨ qinv-≃ (Ξ» {idp β†’ idp}) ( (Ξ» {idp β†’ idp}) , (Ξ» {idp β†’ idp}) , (Ξ» {idp β†’ idp})) ⟩
             Path {A = βˆ‘[ (X , h , Ο†h) ∢ ((βˆ‘[ X ] (βˆ‘[ _ ] Hom X _))) ] _ }
              ((A , f , Ο†A) , pA)
              ((B , g , Ο†B) , pB)
              β‰ƒβŸ¨ simplify-pair (Ξ» {(_ , _ ,  _) β†’ trunc-is-prop}) ⟩
           Path {A = βˆ‘[ _ ] βˆ‘[ _ ]  _ }
              (A , f , Ο†A)
              (B , g , Ο†B)
              β‰ƒβŸ¨ qinv-≃ (Ξ» {idp β†’ (idp , idp) , idp}) (( Ξ» { ((idp , idp) , idp) β†’ idp})
                           ,  (Ξ» {((idp , idp) , idp) β†’ idp}) , Ξ» {idp β†’ idp}) ⟩
              _  β‰ƒβˆŽ

      Face'-is-set ((A , Aβ†Ί@(cyclic-graph Ο†A zero pA) , f) , (p₁ , pβ‚‚) , p₃)
                  ((B , Bβ†Ί@(cyclic-graph Ο†B (succ nB) pB) , g) , (q₁ , qβ‚‚) , q₃)
                    = trunc-elim prop-is-prop (Ξ» {idp β†’ trunc-elim prop-is-prop
                      (Ξ» {idp β†’ Ξ» {()}})
                      pB}) pA

      Face'-is-set ((A , Aβ†Ί@(cyclic-graph Ο†A (succ nA) pA) , f) , (p₁ , pβ‚‚) , p₃)
                  ((B , Bβ†Ί@(cyclic-graph Ο†B zero pB) , g) , (q₁ , qβ‚‚) , q₃)
                    = trunc-elim prop-is-prop (Ξ» {idp β†’ trunc-elim prop-is-prop
                      (Ξ» {idp β†’ Ξ» {()}})
                      pB}) pA

      Face'-is-set f1@(d1@(A , Aβ†Ί@(cyclic-graph Ο†A (succ nA) pA) , f) , (p₁ , pβ‚‚) , p₃)
                  f2@(d2@(B , Bβ†Ί@(cyclic-graph Ο†B (succ nB) pB) , g) , (q₁ , qβ‚‚) , q₃)
                  = trunc-elim prop-is-prop (Ξ» {idp β†’ trunc-elim prop-is-prop
                      (Ξ» {idp β†’ isProp-≃ (≃-sym (≃-trans (Face'-Path-space G 𝕄 f1 f2) equiv))
                          (βˆ‘-prop (β„•-is-set _ _) (Ξ» {idp β†’ βˆ‘-prop
                            (βˆ‘-Cn-isos-is-prop β„“ (succ nA) (succ-n>0 β„“ {nA}) (U G) f p₁ g q₁)
                            (Ξ» _ β†’ Hom-is-set A B _ _)}))})
                      pB}) pA
        where
        open import lib.graph-homomorphisms.classes.EdgeInjective.Lemmas
        open import lib.graph-homomorphisms.Lemmas

        open Hom-Lemma-1 A B
        open Hom-Lemma-2 A B (U G) f g
        equiv : (d1 ≑ d2) ≃ (βˆ‘[ Ξ± ∢ nA ≑ nB ]
                             βˆ‘[ p ∢ βˆ‘[ Ξ± ∢ A ≑ B ] (f ≑ g∘ Ξ±) ]
                              ((tr _ (π₁ p) Ο†A) ≑ Ο†B))
        equiv =
           begin≃
              _
               β‰ƒβŸ¨ qinv-≃ (Ξ» {idp β†’ idp}) ((Ξ» {idp β†’ idp}) , (Ξ» {idp β†’ idp}) , (Ξ» {idp β†’ idp})) ⟩
              Path {A = βˆ‘[ _ ] βˆ‘[ _ ] βˆ‘[ _ ] βˆ‘[ _ ]  _ }
              (nA , A , f , Ο†A , pA)
              (nB , B , g , Ο†B , pB)
               β‰ƒβŸ¨ qinv-≃ (Ξ» {idp β†’ idp}) ( (Ξ» {idp β†’ idp}) , (Ξ» {idp β†’ idp}) , (Ξ» {idp β†’ idp})) ⟩
             Path {A = βˆ‘[ (nX , X , h , Ο†h) ∢ (βˆ‘[ _ ] (βˆ‘[ X ] (βˆ‘[ _ ] Hom X _))) ] _ }
              ((nA , A , f , Ο†A) , pA)
              ((nB , B , g , Ο†B) , pB)
              β‰ƒβŸ¨ simplify-pair (Ξ» {(_ , _ , _ , _) β†’ trunc-is-prop}) ⟩
           Path {A = βˆ‘[ _ ] βˆ‘[ _ ] βˆ‘[ _ ]  _ }
              (nA , A , f , Ο†A)
              (nB , B , g , Ο†B)
          β‰ƒβŸ¨ qinv-≃ (Ξ» {idp β†’ idp , idp}) ((Ξ» {(idp , idp) β†’ idp}) ,
                       (Ξ» {(idp , idp) β†’ idp}) , Ξ» {idp β†’ idp}) ⟩
            ((nA ≑ nB) Γ— Path ((A , f , Ο†A)) ((B , g , Ο†B)))

          β‰ƒβŸ¨ qinv-≃ (Ξ» {(idp , idp) β†’ idp , (idp , idp)}) ((Ξ» {(idp , (idp , idp)) β†’ (idp , idp)}) ,
                (Ξ» {(idp , (idp , idp)) β†’ idp}) , Ξ» {(idp , idp) β†’ idp}) ⟩
            ((nA ≑ nB) Γ— (βˆ‘[ Ξ± ∢ A ≑ B ] (Path (f , tr _ Ξ± Ο†A) (g∘ Ξ± , Ο†B))))
                β‰ƒβŸ¨ qinv-≃ (Ξ» {(idp , (idp , idp)) β†’ idp , (idp , idp) , idp})
                ((Ξ» {(idp , ((idp , idp) , idp)) β†’ idp , (idp , idp )}) ,
                  (Ξ» {(idp , ((idp , idp) , idp)) β†’ idp})
                  , Ξ» {(idp , (idp , idp)) β†’ idp}) ⟩
          ((nA ≑ nB) Γ— (βˆ‘[ p ∢ βˆ‘[ Ξ± ∢ A ≑ B ] (f ≑ g∘ Ξ±) ] ((tr _ (π₁ p) Ο†A) ≑ Ο†B)))
          β‰ƒβˆŽ

    Face-is-set : isSet (Face G 𝕄)
    Face-is-set = equiv-preserves-sets (Face'≃Face G 𝕄) Face'-is-set

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