Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-embeddings.Finiteness
  where
  open import foundations.Core
  open import foundations.HLevelLemmas

  open import foundations.NaturalsType
  open import foundations.Nat

  open import lib.graph-embeddings.Map
  open import lib.graph-embeddings.Map.Face

  open import lib.graph-definitions.Graph
  open Graph

  open import lib.graph-transformations.U

  open import lib.graph-homomorphisms.Hom
  open Hom

  open import lib.graph-classes.CyclicGraph
  open CyclicGraph
  open import lib.graph-classes.CyclicGraph.Stuff
  open import foundations.Cyclic

  open import lib.graph-classes.FiniteGraph
  open import foundations.Finite

  open import lib.graph-homomorphisms.classes.EdgeInjective

  module _
    {ℓ : Level} (G : Graph ℓ)
    (G-is-finite : isFiniteGraph G)
    where

    Nodes-is-finite = isFiniteGraph.NodeDec G-is-finite
    Edges-is-finite = isFiniteGraph.EdgeDec G-is-finite

    _≟Node_ : (x y : Node G) → (x ≡ y) + (x ≠ y)
    _≟Node_ = isFinite-→-isDec Nodes-is-finite
    -- open WR G (_≟Node_)

    Ng : ℕ
    Ng = cardinal (Node G) Nodes-is-finite

    module finiteness-lemmas
      -- The following are well-known lemmas about finite types.
      (+-finite : ∀ {A B : Type ℓ} → isFinite A → isFinite B → isFinite (A + B))
      (∏-finite : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : A → Type ℓ₂}
                → isFinite A → ((a : A) → isFinite (B a)) → isFinite (∏ A B))
      (∑-finite : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : A → Type ℓ₂}
                → isFinite A → ((a : A) → isFinite (B a)) → isFinite (∑ A B))
      where

      U-finite : isFiniteGraph (U G)
      U-finite = U-preserves-finiteness +-finite G G-is-finite

      UNode-is-finite : isFinite (Node (U G))
      UNode-is-finite = isFiniteGraph.NodeDec U-finite
      UEdge-is-finite : ∀ (x y : Node (U G)) → isFinite (Edge (U G) x y)
      UEdge-is-finite x y = isFiniteGraph.EdgeDec U-finite x y


      finite-stars : (x : Node G) → isFinite (Star G x)
      finite-stars x = ∑-finite Nodes-is-finite (λ _ → UEdge-is-finite _ _)

      finite-maps : isFinite (Map G)
      finite-maps = ∏-finite Nodes-is-finite λ x →
        cyclic-set-is-finite ℓ ∏-finite ∑-finite (finite-stars x)

We want to prove that the collection of

      module _ (A : Graph ℓ) (A-is-cyclic : CyclicGraph ℓ A) where
        A-is-finite-graph : isFiniteGraph A
        A-is-finite-graph = CyclicGraph-is-finite A A-is-cyclic
          where
          open import lib.graph-classes.CyclicGraph.isFiniteGraph

        Node-A-is-finite : isFinite (Node A)
        Node-A-is-finite = isFiniteGraph.NodeDec A-is-finite-graph

        Edge-A-is-finite : (x y : Node A) → isFinite (Edge A x y)
        Edge-A-is-finite x y = isFiniteGraph.EdgeDec A-is-finite-graph _ _

        finite-hom : isFinite (Hom A (U G))
        finite-hom
          = equiv-preserves-finiteness (≃-sym (Hom-≃-∑ A (U G)))
            (∑-finite (∏-finite Node-A-is-finite λ _ → UNode-is-finite) λ _
              → ∏-finite Node-A-is-finite λ _
                → ∏-finite Node-A-is-finite λ _
                  → ∏-finite (Edge-A-is-finite _ _) λ _
                  → UEdge-is-finite _ _)

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