Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-relations.Isomorphic
  where
  open import foundations.Core

  open import lib.graph-definitions.Graph
  open import lib.graph-homomorphisms.Hom
  open import lib.graph-homomorphisms.classes.Isomorphisms

  private
    variable
      ℓ ℓ₁ ℓ₂ : Level

  _≅_  _is-isomorphic-to_ : (G : Graph ℓ₁) (H : Graph ℓ₂) →  Type (ℓ₁ ⊔ ℓ₂)
  G ≅ H = ∑[ α ∶ (Node G ≃ Node H) ]
          (∀ (x y : Node G) → Edge G x y ≃ Edge H ((α ∙) x) ((α ∙) y))

  G is-isomorphic-to H = G ≅ H

  module _
    {G : Graph ℓ₁} {H : Graph ℓ₂}
    where

    is-iso-to-≅
      : (h : Hom G H) (iso : IsoHom h)
      ------------------
      → G ≅ H

    is-iso-to-≅  h iso = α-≃ , β-≃
      where open hom-from-iso {G = G} h iso

    ≅-to-is-iso
      :  G ≅ H
      → ∑[ h ∶ Hom G H ] (IsoHom h)

    ≅-to-is-iso iso =
      (hom ((π₁ iso) ∙→) λ x y → (π₂ iso x y) ∙→)
      , (π₂ (π₁ iso) , λ x y → π₂ (π₂ iso x y))

    hom-from-iso
      : G ≅ H
      → Hom G H
    hom-from-iso iso = π₁ (≅-to-is-iso iso)
    syntax hom-from-iso iso = ≅-to-hom iso

    ≅-≃-iso
      : (G ≅ H) ≃ (∑[ h ∶ Hom G H ] (IsoHom h))
    ≅-≃-iso = qinv-≃ ≅-to-is-iso
      ((λ {(h , h-is-iso) → is-iso-to-≅ h h-is-iso}) ,
        (λ {h → idp}) , (λ {h → idp }))

\end{definition}

    IsoHom-is-set : (h : Hom G H) → isSet (IsoHom h)
    IsoHom-is-set (hom α₁ β₁)
      = ∑-set (prop-is-set (isEquivIsProp α₁)) $ λ a →
              pi-is-set (λ b →
                pi-is-set (λ c →
                  prop-is-set (isEquivIsProp _ )))

  Aut : (G : Graph ℓ) → Type ℓ
  Aut G = G ≅ G

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