Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-definitions.Graph.EquivalencePrinciple
  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

Equivalence principle

  module EquivPrinciple {ℓ : Level} (G H : Graph ℓ) where
    private
      F₁ : (X : Type ℓ) → Type (lsuc ℓ)
      F₁ X = (X → X → Type ℓ)

      F₂ : (X : Type ℓ)(R : (x y : X) → Type ℓ) → Type ℓ
      F₂ X R = (x y : X) → (R x y) is-set

      nG = Node G
      nH = Node H
      eG = Edge G
      eH = Edge H
      nG-set = Node-is-set G
      nH-set = Node-is-set H
      eG-set = Edge-is-set G
      eH-set = Edge-is-set H

    equiv-principle : (G ≡ H) ≃ (G ≅ H)
    equiv-principle =
      begin≃
        (G ≡ H)                                                      ≃⟨ i ⟩
        ∑[ α ∶ nG ≡ nH ] ∑[ β ∶ tr F₁ α eG ≡ eH ]
             (tr isSet α nG-set ≡ nH-set)
           × (tr₂ F₂ α β eG-set ≡ eH-set)                            ≃⟨ ii ⟩
        ∑[ α ] (tr F₁ α eG ≡ eH)                                     ≃⟨ sigma-preserves iii ⟩
        ∑[ α ] (∀ x y → eG x y ≡ eH (coe α x) (coe α y))             ≃⟨ sigma-preserves iv ⟩
        ∑[ α ] (∀ x y → eG x y ≃ eH (coe α x) (coe α y))             ≃⟨ v  ⟩
        ∑[ α ∶ nG ≃ nH ] (∀ x y → eG x y ≃ eH ((α ∙) x) ((α ∙) y))   ≃⟨⟩
        (G ≅ H)
        ≃∎
      where
      open import foundations.UnivalenceAxiom

      i : (G ≡ H)
          ≃ (Σ[ α ∶ nG ≡ nH ] Σ[ β ∶ tr F₁ α (eG) ≡ eH ] (tr isSet α (nG-set) ≡ nH-set)
                                                      × (tr₂ F₂ α β (eG-set) ≡ (eH-set)))

      i = ≃-sym (qinv-≃ (λ { (idp , idp , idp , idp) → idp})
          ( (λ {idp → idp , idp , idp , idp })
          , (λ { idp → idp}) , λ { (idp , idp , idp , idp) → idp}
          ))
      
      ii =  ≃-sym $
        qinv-≃
        -- functions:
          (λ {(α , β ) → α , β , set-is-prop _ _ 
                       , pi-is-prop (λ a → pi-is-prop (λ b → set-is-prop)) _ (eH-set) })
          ((λ { (α , β , _) → α , β })
        -- homotopies:
        , ((λ {(α , (β , _))
             → pair= (idp
             , pair= (idp , ispropA×B (prop-is-set 
                             (pi-is-prop (λ x → pi-is-prop (λ y → prop-is-prop))) _ (nH-set))
               (prop-is-set (pi-is-prop (λ x → pi-is-prop (λ y → set-is-prop))) _ (eH-set)) _ _))}
        ), λ {(a , b) → idp}))

      iii : (α : nG ≡ nH)  → (tr F₁ α (eG) ≡ eH) ≃ ((x y : nG) → eG x y ≡ eH (coe α x) (coe α y))
      iii idp =
        (eG ≡ eH)                    ≃⟨ eqFunExt ⟩
        (∀ x → (eG x ≡ eH x))        ≃⟨ pi-equivalence (λ w → eqFunExt) ⟩
        (∀ x y → (eG x y ≡ eH x y))  ≃∎ 
        where open import foundations.FunExtAxiom

      iv : (α : nG ≡ nH)
         →  ((x y : nG) → eG x y  ≡ eH (coe α x) (coe α y))
         ≃  ((x y : nG) → eG x y  ≃  eH (coe α x) (coe α y))
      iv idp = pi-equivalence $ λ x → pi-equivalence $ λ y → eqvUnivalence
        
      v  =  ≃-sym (sigma-preserves-≃ eqvUnivalence)

    -- Other alias
    ≡-≃-≅ : (G ≡ H) ≃ (G ≅ H)
    ≡-≃-≅ = equiv-principle

    ≡-from-iso : (G ≅ H) → (G ≡ H)
    ≡-from-iso = rapply equiv-principle

    ≡-→-≅ :  (G ≡ H) → (G ≅ H)
    ≡-→-≅ = apply equiv-principle

    computation-rule₁
      : (e : G ≅ H)
      → (≡-≃-≅ ∙→) ((≡-≃-≅ ∙←) e) ≡ e
    computation-rule₁ e = lrmap-inverse-h {A = G ≡ H} {B = G ≅ H} ≡-≃-≅ e

    computation-rule₂
      : (e : G ≡ H)
      → (≡-≃-≅ ∙←) ((≡-≃-≅ ∙→) e) ≡ e
    computation-rule₂ e = rlmap-inverse-h  {A = G ≡ H} {B = G ≅ H} ≡-≃-≅ e
    -- NOTE: If I replace ≡-≃-≅ ∙→ by ≡-≃-≅, this doesn't typecheck, why not?

    ≡-≡-≅ : (G ≡ H) ≡ ↑ _ (G ≅ H)
    ≡-≡-≅ = ua (≃-trans equiv-principle (lifting-equivalence _))
      where
      open import foundations.UnivalenceAxiom

Leibniz’s property

Isomorphic graphs hold the same propositional properties.

  leibniz 
    : {ℓ : Level} (G H : Graph ℓ)
    → G ≅ H → (P : Graph ℓ → Type ℓ)  → (P G → P H)
  leibniz G H G≡H P PG = tr P (rapply (equiv-principle G H) G≡H) PG
    where open EquivPrinciple

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