Investigations on graph-theoretical constructions in Homotopy type theory

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

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

  private
    variable
      ℓ ℓ₁ ℓ₂ : Level

Edge-injectivity homomorphim:

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

    isEdgeInj : Hom G H → Type (ℓ₁ ⊔ ℓ₂)
    isEdgeInj (hom α β)
      = ∀ {x y : Node G}   → (e₁ : Edge G x y)
      → ∀ {x' y' : Node G} → (e₂ : Edge G x' y')
      → Path {A = ∑[ x ] ∑[ y ] Edge H x y}
          (α x  , α y  , β x  y  e₁)
          (α x' , α y' , β x' y' e₂)
      -------------------------------
      → (x , y , e₁) ≡ (x' , y' , e₂)

    being-edge-inj-is-prop
      : (h : Hom G H) → isProp (isEdgeInj h)
    being-edge-inj-is-prop h =
      pi-is-prop-implicit λ a → pi-is-prop-implicit $ λ b
        → pi-is-prop $ λ e₁ → pi-is-prop-implicit $ λ x →
        pi-is-prop-implicit $ λ y → pi-is-prop $ λ e₂ → pi-is-prop $ λ p →
          ∑-set (Node-is-set G) (λ _ → ∑-set (Node-is-set G) (λ e → Edge-is-set 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