Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-homomorphisms.Hom
  where
  open import foundations.Core

  open import lib.graph-definitions.Graph
  open Graph public

  private
    variable
      ℓ₁ ℓ₂ : Level

  record
    Hom (G : Graph ℓ₁) (H : Graph ℓ₂)
      : Type (ℓ₁ ⊔ ℓ₂)
    where
    eta-equality
    constructor hom
    field
      α : Node G → Node H
      β : (x y : Node G) → Edge G x y → Edge H (α x) (α y)

  syntax hom α β = ⟨ α , β ⟩

  Hom-≃-∑
    : (G : Graph ℓ₁) (H : Graph ℓ₂)
    → Hom G H ≃ (∑[ α ∶ (Node G → Node H) ]
              ((x y : Node G) → Edge G x y → Edge H (α x) (α y)))

  Hom-≃-∑ G H = qinv-≃ f (g , (λ {x → idp}) , λ {x → idp})
      where
      private
        f : Hom G H → ∑ (Node G → Node H)
          (λ α → (x y : Node G) → Edge G x y → Edge H (α x) (α y))
        f (hom α β) = α , β

        g : ∑ (Node G → Node H)
          (λ α → (x y : Node G) → Edge G x y → Edge H (α x) (α y))
          → Hom G H
        g (α , β) = hom α β

  abstract
    Hom-is-set
      : (G : Graph ℓ₁) (H : Graph ℓ₂)
      → isSet (Hom G H)

    open import foundations.UnivalenceAxiom
    Hom-is-set G H 
      = equiv-preserves-sets (≃-sym (Hom-≃-∑ G H)) 
        (isSet-Σ (∏-set (λ _ → Node-is-set H))
              λ α → ∏-set
                (λ x → ∏-set
                  (λ y → pi-is-set (λ a → Edge-is-set H _ _))))

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

    _∘Hom_ : Hom G H → Hom H K → Hom G K
    (hom α₁ β₁) ∘Hom (hom α₂ β₂)
      = hom (α₁ ︔ α₂) (λ x y e → β₂ (α₁ x) (α₁ y) (β₁ x y e))

  _hom≅_
    : ∀ {ℓ₁ ℓ₂ : Level}
    → (G : Graph ℓ₁) → (H : Graph ℓ₂) → Type (ℓ₁ ⊔ ℓ₂)
  G hom≅ H = Hom G H × Hom H G

  module _ {ℓ : Level}(G : Graph ℓ) where
    id-hom : Hom G G
    id-hom = hom identity (λ _ _ e → e)

  module _ {ℓ : Level}{G : Graph ℓ}
    where
    expo-hom : ℕ → (φ : Hom G G) → Hom G G
    expo-hom  φ        = id-hom G
    expo-hom (succ n) φ = expo-hom n φ ∘Hom φ

    syntax expo-hom n h = h ^-hom n

    open Hom
    lemma-on-nodes-hom-expo
      : (φ : Hom G G) → (n : ℕ)
      → ((α φ) ^ n) ≡ α (expo-hom n φ)


    lemma-on-nodes-hom-expo φ  = idp
    lemma-on-nodes-hom-expo φ (succ n)
      = funext (λ e → ap (α φ)
               (happly (lemma-on-nodes-hom-expo φ n) e))
      where open import foundations.FunExtAxiom

  ∘Hom-assoc
    : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {G : Graph ℓ₁}{H : Graph ℓ₂}{K : Graph ℓ₃}{L : Graph ℓ₄}
    → (f : Hom G H) (g : Hom H K) (h : Hom K L)
    -----------------------------------------------------------------
    → ((f ∘Hom g) ∘Hom h) ≡ (f ∘Hom (g ∘Hom h))
  ∘Hom-assoc f g h = idp

  _has-hom-property_
    : ∀ {ℓ₁ ℓ₂ : Level} {G : Graph ℓ₁} {H : Graph ℓ₂}
      → (h : Hom G H)
      → (P : ∀ {ℓ₁}{ℓ₂}{X}{Y} → Hom {ℓ₁}{ℓ₂} X Y → hProp (ℓ₁ ⊔ ℓ₂))
      → Type (ℓ₁ ⊔ ℓ₂)

  h has-hom-property P = π₁ (P h)

  _has-endo-hom-property_
     : ∀ {ℓ : Level} {H : Graph ℓ}(h : Hom H H)
     → (P : ∀ {X} → Hom X X → hProp ℓ)
     → Type ℓ
  h has-endo-hom-property P = π₁ (P 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