Investigations on graph-theoretical constructions in Homotopy type theory

Cyclic Stuff

  open import lib.graph-families.CycleGraph
  open import lib.graph-families.CycleGraph.RotHom

  record
    CyclicGraph (ℓ : Level) (G : Graph ℓ) : Type (lsuc ℓ)
    where
    eta-equality
    constructor cyclic-graph
    field
      φ : Hom G G
      n : ℕ
      is-cyclic : ∥ Path {A = ∑[ H ] (Hom H H)} (G , φ) (Cycle ℓ n , rot ℓ n) ∥

  _is-cyclic-graph = CyclicGraph

  same-cyclic-graph :  (ℓ : Level) (G : Graph ℓ)
     → (A-cyclic@(cyclic-graph f n c) : CyclicGraph ℓ G)
     → (d : ∥ Path {A = ∑[ H ] (Hom H H)} (G , f) (Cycle ℓ n , rot ℓ n) ∥)
     → (cyclic-graph f n d ≡ A-cyclic)
  same-cyclic-graph ℓ G (cyclic-graph f n c) d = ! β
    where
    α : c ≡ d
    α = trunc-is-prop c d
    β : (cyclic-graph f n c) ≡ (cyclic-graph f n d)
    β = ap (cyclic-graph f n) α

  module CyclicGraph-is-set {ℓ : Level}{G : Graph ℓ}
    where
    ∑s : Type (lsuc ℓ)
    ∑s = ∑[ φ ∶ Hom G G ] ∑[ n  ∶ ℕ ]
         ∥ Path {A = ∑[ H ] (Hom H H)} (G , φ) (Cycle ℓ n , rot ℓ n) ∥

    CyclicGraph-≃-∑s : ∑s ≃ CyclicGraph ℓ G
    CyclicGraph-≃-∑s = qinv-≃
        (λ { (f , n , c) → cyclic-graph f n c})
          ((λ {cset → φ cset , n cset , is-cyclic cset})
          , (λ {p → idp}) , λ {p → idp})
        where open CyclicGraph

    ∑s-is-set : isSet ∑s
    ∑s-is-set = ∑-set (Hom-is-set G G)
        (λ f → ∑-set ℕ-is-set (λ _ → prop-is-set truncated-is-prop))

    proof : isSet (CyclicGraph ℓ G)
    proof = ≃-with-a-set-is-set CyclicGraph-≃-∑s ∑s-is-set

  open import foundations.NaturalsType

  instances-have-same-natural
    : (ℓ : Level) (G : Graph ℓ)
    → (f1 f2 : CyclicGraph ℓ G)
    → (CyclicGraph.n f1 ≡ CyclicGraph.n f2)
  instances-have-same-natural ℓ G (cyclic-graph f n c) (cyclic-graph g m d)
    = trunc-elim (ℕ-is-set _ _)
      (λ { idp →
      trunc-elim (ℕ-is-set _ _) (λ {o →
        let helper : Cycle ℓ n ≡ Cycle ℓ m
            helper = π₁ (apply pair-≃-∑ o)
        in Cycle-is-inj ℓ n m helper})
        d}) c

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