lib.graph-families.CycleGraph.Walk.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 --allow-unsolved-metas #-}
module lib.graph-families.CycleGraph.Walk
where
open import foundations.Core
open import lib.graph-definitions.Graph
open Graph
module
_
(ℓ : Level)
where
open import foundations.Nat ℓ
open import foundations.Fin ℓ
open import lib.graph-families.CycleGraph ℓ
open import lib.graph-embeddings.Map
open import lib.graph-transformations.U
open import lib.graph-families.CycleGraph.Map
open import lib.graph-families.CycleGraph.isCyclicGraph
open import lib.graph-classes.CyclicGraph.Walk
open import lib.graph-walks.Walk
open import lib.graph-walks.Walk.QuasiSimple
module
_ (n : ℕ)
where
-- Between two points in U(Cn), we always have two simple walks CW- and CCW-.
ccw
: (a b : Node (Cycle n))
------------------------
→ Walk (U (Cycle n)) a b
ccw = ccw-walk (Cycle n) (Cn-is-cyclic-graph ℓ n)
where open UndirectedWalks
cw
: (a b : Node (Cycle n))
------------------------
→ Walk (U (Cycle n)) a b
cw = cw-walk (Cycle n) (Cn-is-cyclic-graph ℓ n)
where open UndirectedWalks
-- open lib.graph-walks.Walk.QuasiSimple.simplewalks
-- cw-is-simple
-- : (n : ℕ)
-- → (x y : Node (Cycle n))
-- → (cw n x y) is-quasi-simple
-- cw-is-simple = {!!}
-- cw-is-simple zero (x , <0) _ = ⊥-elim {ℓ} (n<0 {ℓ}{n = x} <0)
-- cw-is-simple (succ n) x y = {!cw-is-simple n !}
-- ccw-is-simple
-- : (n : ℕ)
-- → (x y : Node (Cycle n))
-- → (ccw n x y) is-quasi-simple
-- {-
-- f
-- : (n : ℕ)
-- → (x y : Node (Cycle n))
-- → ((x ≡ y) × 𝟛 ℓ) + ((x ≠ y) × 𝟚 ℓ)
-- → ∑[ w ∶ Walk (U (Cycle n)) x y ] (w is-quasi-simple)
-- f n x .x (inl (idp , 𝟘₃)) = (⟨ x ⟩ , one-point-walk-is-simple {G = U (Cycle n)} x)
-- f n x .x (inl (idp , 𝟙₃)) = (ccw n x x , ccw-is-simple n x x)
-- f n x .x (inl (idp , 𝟚₃)) = (cw n x x , cw-is-simple n x x)
-- f n x y (inr (x≠y , 𝟘₂)) = (ccw n x y , ccw-is-simple n x y)
-- f n x y (inr (x≠y , 𝟙₂)) = (cw n x y , cw-is-simple n x y)
-- -}
-- {-
-- g
-- : (n : ℕ)
-- → (x y : Node (Cycle n))
-- → (w : Walk (U (Cycle n)) x y)
-- → w is-quasi-simple
-- → (x ≡ y) + ((w ≡ ccw n x y) + (w ≡ cw n x y))
-- g zero (zero , ()) y w w-is-simple
-- g zero (succ π₃ , ()) y w w-is-simple
-- g (succ zero) (zero , ∗) (zero , ∗) ⟨ .(0 , ∗) ⟩ w-is-simple = inl idp
-- g (succ zero) (zero , ∗) (zero , ∗) (inl x ⊙ w) w-is-simple = {!!}
-- -- = inr (inl {!!})
-- g (succ zero) (zero , ∗) (zero , ∗) (inr x ⊙ w) w-is-simple = inr (inr {!idp!})
-- g (succ zero) (zero , _) (succ zero , ()) w w-is-simple
-- g (succ zero) (zero , _) (succ (succ _) , ()) w w-is-simple
-- g (succ zero) (succ zero , ()) (zero , π₆) w w-is-simple
-- g (succ zero) (succ (succ _) , ()) (zero , π₆) w w-is-simple
-- g (succ zero) (succ zero , ()) (succ π₅ , π₆) w w-is-simple
-- g (succ zero) (succ (succ _) , ()) (succ π₅ , π₆) w w-is-simple
-- g (succ (succ n)) x y w w-is-simple = {!!}
-- -}
-- {-
-- f-is-equiv
-- : (n : ℕ)(x y : Node (Cycle n))
-- → (f n x y) is-equiv
-- f-is-equiv zero (zero , ()) _
-- f-is-equiv zero (succ _ , ()) _
-- -- ≡ 1
-- f-is-equiv (succ zero) x@(zero , ∗) (zero , ∗)
-- = λ { (⟨ .(0 , ∗) ⟩ , w-is-simple)
-- → ( -- center of the contraction
-- ((inl (idp , 𝟘₃) , pair= (idp , being-simple-is-prop {G = U (Cycle _)} (⟨ x ⟩) _ _)))
-- -- proof it's indeed a center the above term.
-- , λ { (inl (idp , 𝟘₃) , idp) → pair= (idp ,
-- {!!}
-- )
-- ; (inl (idp , 𝟙₃) , π₄) → {!π₄!}
-- ; (inl (idp , 𝟚₃) , π₄) → {!!}
-- ; (inr (x≠x , π₅) , π₄) → ⊥-elim (x≠x idp)})
-- ; ((x ⊙ p) , q) → {!!}}
-- f-is-equiv (succ zero) (zero , _) (succ zero , ())
-- f-is-equiv (succ zero) (zero , _) (succ (succ _) , ())
-- f-is-equiv (succ zero) (succ zero , ()) (zero , ∗)
-- f-is-equiv (succ zero) (succ (succ _) , ()) (zero , _)
-- -- ≡ 2
-- f-is-equiv (succ (succ zero)) (π₃ , π₄) (π₅ , π₆) = {!!}
-- -- >= 3
-- f-is-equiv (succ (succ (succ n))) x y = {!!}
-- -}
-- {-
-- Cn-walk-equiv
-- : (n : ℕ) → (x y : Node (Cycle n))
-- → ((x ≡ y) × 𝟛 ℓ) + ((x ≠ y) × 𝟚 ℓ)
-- ≃ (∑[ w ∶ Walk (U (Cycle n)) x y ] (w is-quasi-simple))
-- Cn-walk-equiv n x y = (f n x y , f-is-equiv n x y)
-- -}
-- -- open import lib.graph-classes.Planar
-- ```
(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