Investigations on graph-theoretical constructions in Homotopy type theory

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

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

The following is the version of isomorphisms induction, based on the proof given by Escardo on .

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

  module
    _
    {ℓ : Level}
    (G : Graph ℓ)
    where

    isomorphism-induction
      : (P : (H : Graph ℓ) → (G ≅ H) → Type ℓ)
      → P G (id-≅ G)
      → (H : Graph ℓ) → (h : G ≅ H)
      -----------------------------
      → P H h

    isomorphism-induction P P-id-iso H h = tr (P H) comp-rule-≅ g
      where
      open import lib.graph-definitions.Graph.EquivalencePrinciple
      open EquivPrinciple

      private
        P' :  (H : Graph ℓ) → G ≡ H → Type ℓ
        P' H p = P H ((equiv-principle G H ∙→) p)

        b' : P G ((equiv-principle G G ∙→) (refl G))
        b' = P-id-iso

        f' : (H : Graph ℓ) → (p : G ≡ H) → P' H p
        f' H idp = b'

        g : P H ((equiv-principle G H ∙→) ((equiv-principle G H ∙←) h))
        g = f' H ((equiv-principle G H ∙←) h)

        comp-rule-≅ : ((equiv-principle G H ∙→) ((equiv-principle G H ∙←) h)) ≡ h
        comp-rule-≅ = computation-rule₁ G H h

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