lib.graph-families.CycleGraph.md.
Version of Sunday, January 22, 2023, 10:42 PM
Powered by agda version 2.6.2.2-442c76b and pandoc 2.14.0.3
{-# OPTIONS --without-K --exact-split #-}
open import foundations.Core using (Level)
module lib.graph-families.CycleGraph (ℓ : Level)
where
open import foundations.Core
open import lib.graph-definitions.Graph
open Graph
open import foundations.Fin ℓ
renaming (fin-pred to pred ; fin-suc to suc)
open import lib.graph-classes.UnitGraph
open import lib.graph-relations.Isomorphic
Cycle : ℕ → Graph ℓ
Cycle zero = 𝟙-graph ℓ
Cycle (succ n) = graph ⟦ succ n ⟧
(λ x y → x ≡ pred y)
(Fin-is-set)
(λ _ _ → set-is-groupoid Fin-is-set _ _)
syntax Cycle n = ℂ n
module _ where
open import lib.graph-classes.UnitGraph
Cycle-is-inj : (n m : ℕ) → Cycle n ≡ Cycle m → n ≡ m
Cycle-is-inj zero zero _ = idp
Cycle-is-inj zero (succ m) Cn=Cm
= ⊥-elim (π₂ (π₂ (v (pred (zero , unit) , (zero , unit) , idp))))
where
v : (∑[ x ] ∑[ y ] Edge (Cycle (succ m)) x y)
→ (∑[ x ] ∑[ y ] Edge (𝟙-graph ℓ) x y)
v f = tr (λ G → ∑[ x ] ∑[ y ] Edge G x y) (! Cn=Cm) f
Cycle-is-inj (succ n) zero Cn=Cm
= ⊥-elim (π₂ (π₂ (v (pred (zero , unit) , (zero , unit) , idp))))
where
v : ∑[ x ] ∑[ y ] Edge (Cycle (succ n)) x y
→ ∑[ x ] ∑[ y ] Edge (𝟙-graph ℓ) x y
v f = tr (λ G → ∑[ x ] ∑[ y ] Edge G x y) Cn=Cm f
Cycle-is-inj (succ n) (succ m) Cn=Cm
= Fin₁-is-inj-≃ (succ n) (succ m) (π₁ (apply (equiv-principle) Cn=Cm))
where
open import lib.graph-definitions.Graph.EquivalencePrinciple
open EquivPrinciple (Cycle (succ n)) (Cycle (succ m))
Edge-Cn-is-prop
: ∀ {n}{x y : Node (ℂ n)}
→ isProp (Edge (ℂ n) x y)
Edge-Cn-is-prop {n = succ n} {x}{y} = Fin-is-set _ _
-- However, in the undirected version of a this graph,
-- the above lemma only holds when n≥3.
open import lib.graph-transformations.U
open import foundations.Nat ℓ
Edge-Undirected-Cn-is-prop
: ∀ {n : ℕ}
→ (x y : Node (Cycle (n +ℕ 3 )))
→ isProp (Edge (U (Cycle (n +ℕ 3))) x y)
Edge-Undirected-Cn-is-prop {zero} x y
= +-prop (Edge-Cn-is-prop {n = 3} {y = y})
(Edge-Cn-is-prop {n = 3}) λ {(p , q ) → helper (p , q)}
where
helper : ¬ (Edge (Cycle 3) x y × Edge (Cycle 3) y x)
helper (p , q) rewrite p
= ⊥-from-fin-predx=y+x=fin-predy {k = 0} (ap pred p · ! q) p
Edge-Undirected-Cn-is-prop {n@(succ _)} x y
= +-prop (Edge-Cn-is-prop {succ _}) (Edge-Cn-is-prop {succ _}) helper
where
helper : ¬ (Edge (Cycle (n +ℕ 3)) x y × Edge (Cycle (n +ℕ 3)) y x)
helper (p , q) rewrite p = ⊥-from-fin-predx=y+x=fin-predy {k = n} (ap pred p · ! q) p
module
_
{n : ℕ}
(x : Node (ℂ succ n))
where
with-pred : Edge (ℂ succ n) (pred x) x
with-pred = refl (pred x)
with-pred-is-prop : isProp (Edge (ℂ succ n) (pred x) x)
with-pred-is-prop x = Fin-is-set _ _ _
with-succ : Edge (ℂ succ n) x (suc x)
with-succ = ! fin-pred∘inverse-of-fin-pred x
with-suc-is-prop : isProp (Edge (ℂ succ n) x (suc x))
with-suc-is-prop x = Fin-is-set _ _ _
(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