Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-classes.FiniteGraph
  where
  open import foundations.Core
  open import lib.graph-definitions.Graph
  open Graph

  module _ {ℓ : Level} where
    open import foundations.Finite using (isFinite; being-finite-is-prop)

    record
      isFiniteGraph (G : Graph ℓ)
        : Type ℓ
      where
      constructor finite-graph
      field
        NodeDec : isFinite (Node G)
        EdgeDec : (x y : Node G) → isFinite (Edge G x y)
    open isFiniteGraph

    {-
    number-of-vertices number-of-edges : ℕ
    number-of-vertices = cardinal (Node G) NodeDec
    number-of-edges    = cardinal ( (x y : Node G) → Edge G x y)
      (∏-finite NodeDec λ x → ∏-finite NodeDec λ y → EdgeDec x y)
    -}

    isFiniteGraph-∑
      : (G : Graph ℓ)
      → (isFiniteGraph G)
      ≃ (∑[ NodeDec ∶ isFinite (Node G) ] ((x y : Node G) → isFinite (Edge G x y)))
    isFiniteGraph-∑ G = qinv-≃ (λ {(finite-graph nd ed) → (nd , ed)})
                  ((λ {(nd , ed) → finite-graph nd ed}) , (λ {p → idp})  , λ {p → idp})

    being-finite-graph-is-prop
      : ∀ {G : Graph ℓ}
      → isProp (isFiniteGraph G)

    being-finite-graph-is-prop {G = G}
      = equiv-preserves-prop 
        (≃-sym (isFiniteGraph-∑ G)) 
        (∑-prop being-finite-is-prop
            (λ _ → pi-is-prop (λ _ →
                    pi-is-prop (λ _ →
                      being-finite-is-prop))))

    open import lib.graph-transformations.U
    module _
      (+-finite : ∀ {A B : Type ℓ} → isFinite A → isFinite B → isFinite (A + B))
      where

      U-preserves-finiteness
          : ∀ (G : Graph ℓ)
          → isFiniteGraph G
          → isFiniteGraph (U G)
      NodeDec (U-preserves-finiteness G G-is-finite) = NodeDec G-is-finite
      EdgeDec (U-preserves-finiteness G G-is-finite) x y
        = +-finite (EdgeDec G-is-finite x y) (EdgeDec G-is-finite y x)

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