Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-families.CycleGraph.isFiniteGraph
  where
  open import foundations.Core
  open import lib.graph-definitions.Graph
  open Graph

  module _ {ℓ : Level}
    where
    open import lib.graph-classes.FiniteGraph
    open import foundations.Finite
    open import foundations.Fin
    open import lib.graph-families.CycleGraph ℓ

    _≟Node_ : (n : ℕ) (x y : Node (Cycle n)) → (x ≡ y) + (x ≠ y)
    _≟Node_ zero x y = isFinite-→-isDec 𝟙-is-finite _ _
    _≟Node_ (succ n) x y = Fin-is-decidable ℓ x y

    _≟Edge_ : (n : ℕ) → {x y : Node (Cycle n)}
          → (e₁ e₂ : Edge (Cycle n) x y)
          → (e₁ ≡ e₂) + (e₁ ≠ e₂)
    _≟Edge_ zero e₁ e₂ = isFinite-→-isDec 𝟘-is-finite _ _
    _≟Edge_ (succ n) e₁ e₂
      = isFinite-→-isDec (decidable-→-≡-is-finite (_≟Node_ (succ n)) _ _) e₁ e₂
        where
        x = source (Cycle (succ n)) e₁
        y = target (Cycle (succ n)) e₁

    Cycle-graph-is-finite : (n : ℕ) → isFiniteGraph (Cycle n)
    isFiniteGraph.NodeDec (Cycle-graph-is-finite zero) = 𝟙-is-finite
    isFiniteGraph.EdgeDec (Cycle-graph-is-finite zero) = λ _ _ → 𝟘-is-finite
    isFiniteGraph.NodeDec (Cycle-graph-is-finite (succ n)) = Fin-is-finite
    isFiniteGraph.EdgeDec (Cycle-graph-is-finite (succ n)) x y
      = decidable-→-≡-is-finite (_≟Node_ (succ n)) _ _

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