Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-homomorphisms.classes.Isomorphisms
  where
  open import foundations.Core
  open import lib.graph-definitions.Graph
  open import lib.graph-homomorphisms.Hom
  open Hom

  private
    variable
      ℓ ℓ₁ ℓ₂ : Level

  IsoHom : ∀ {G : Graph ℓ₁}{H : Graph ℓ₂} (h : Hom G H) →  Type (ℓ₁ ⊔ ℓ₂)
  IsoHom {G = G} {H} h = (isEquiv (α h)) × ((x y  : Node G) → isEquiv ((β h) x y))

  id-iso : (G : Graph ℓ) → IsoHom (id-hom G)
  id-iso G =  (proj₂ $ idEqv {A = Node G}) , λ x y → proj₂ $ idEqv {A = Edge G x y}

Given a graph homomorphism \(h\), it is a proposition that \(h\) is an isomorphism.

  being-iso-is-prop
    : ∀ {G : Graph ℓ₁}{H : Graph ℓ₂}
    → (h : Hom G H) → isProp (IsoHom h)

  being-iso-is-prop h =
    ×-is-prop
      (is-equiv-is-prop _)
      (pi-is-prop (λ x → pi-is-prop (λ x → is-equiv-is-prop _)))

  module hom-from-iso
    {ℓ₁ ℓ₂ : Level} {G : Graph ℓ₁}{H : Graph ℓ₂} (h : Hom G H) (iso : IsoHom h)
    where
    open Hom

    private
      α-equiv = π₁ iso
      β-equiv = π₂ iso

    α-≃ : Node G ≃ Node H
    α-≃ = (α h , α-equiv)

    β-≃ : (x y : Node G) → Edge G x y ≃ Edge H (α h x) (α h y)
    β-≃ x y = (β h _ _) , (β-equiv _ _)

    α⁻¹ : Node H → Node G
    α⁻¹ = remap α-≃

    β⁻¹-≃ : (x y : Node H) → Edge H x y ≃ Edge G (α⁻¹ x) (α⁻¹ y)
    β⁻¹-≃ x y =
      begin≃
        Edge H x y
          ≃⟨ idtoeqv (ap² (Edge H)
                     (! (lrmap-inverse-h α-≃ x))
                     (! (lrmap-inverse-h α-≃ y))) ⟩
        Edge H (α h (α⁻¹ x)) (α h (α⁻¹ y))
          ≃⟨ ≃-sym (β-≃ _ _) ⟩
        Edge G (α⁻¹ x) (α⁻¹ y)
      ≃∎ where open import foundations.UnivalenceAxiom

    inv-from-iso : Hom H G
    inv-from-iso = hom α⁻¹ (λ x y → (β⁻¹-≃ x y) ∙→)

    inv-from-iso-is-iso : IsoHom inv-from-iso
    inv-from-iso-is-iso = π₂ (≃-sym α-≃) , λ x y → π₂ (β⁻¹-≃ x y)

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