lib.graph-walks.Walk.Composition.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 #-}
module lib.graph-walks.Walk.Composition
where
open import foundations.Core
open import lib.graph-definitions.Graph
open Graph
open import lib.graph-walks.Walk renaming (length to len)
private
variable
ℓ : Level
module ∙-walk (G : Graph ℓ) where
open import foundations.Nat ℓ
length = len G
private
variable
x y z w : Node G
_·w_ : Walk G x y → Walk G y z → Walk G x z
⟨ x ⟩ ·w w₂ = w₂
(e ⊙ p) ·w q = e ⊙ (p ·w q)
infixr 5 _·w_ _∙w_
_∙w_ = _·w_
_⊙b_ : ∀ {x y z} → Walk G x y → Edge G y z
→ Walk G x z
⟨ _ ⟩ ⊙b e = e ⊙ ⟨ _ ⟩
(x ⊙ w) ⊙b e = x ⊙ (w ⊙b e)
_·w'_
: Walk' G x y → Walk' G y z
→ Walk' G x z
w1 ·w' ⟨ _ ⟩' = w1
w1 ·w' (w2 ⊙' x) = (w1 ·w' w2) ⊙' x
infixr 5 _·w'_
walk : ∀ {x y} → Walk' G x y → Walk G x y
walk ⟨ _ ⟩' = ⟨ _ ⟩
walk (w ⊙' e) = (walk w) ∙w (e ⊙ ⟨ _ ⟩)
walk' : ∀ {x y} → Walk G x y → Walk' G x y
walk' ⟨ _ ⟩ = ⟨ _ ⟩'
walk' (e ⊙ w) = (⟨ _ ⟩' ⊙' e) ·w' walk' w
∙w-assoc
: (w₁ : Walk G x y)(w₂ : Walk G y z)(w₃ : Walk G z w)
→ ((w₁ ∙w w₂) ∙w w₃) ≡ (w₁ ∙w (w₂ ∙w w₃))
∙w-assoc ⟨ _ ⟩ _ _ = idp
∙w-assoc (k ⊙ w₁) w₂ w₃ = ap (λ p → k ⊙ p) (∙w-assoc w₁ w₂ w₃)
∙w-assoc-four-walks
: ∀ {x y z w v}
→ ∀ (w₁ : Walk G x y)(w₂ : Walk G y z)(w₃ : Walk G z w)(w₄ : Walk G w v)
→ ((w₁ ·w (w₂ ∙w w₃)) ∙w w₄)
≡ (w₁ ·w (w₂ ∙w (w₃ ∙w w₄)))
∙w-assoc-four-walks w₁ w₂ w₃ w₄
= begin
((w₁ ·w (w₂ ∙w w₃)) ∙w w₄)
≡⟨ ∙w-assoc w₁ _ _ ⟩
(w₁ ·w ((w₂ ∙w w₃) ∙w w₄))
≡⟨ ap (w₁ ∙w_) (∙w-assoc _ w₃ w₄) ⟩
(w₁ ·w (w₂ ∙w (w₃ ∙w w₄)))
∎
pointless
: ∀ {x y} {w : Walk G x y}
→ (w ∙w ⟨ y ⟩) ≡ w
pointless {w = ⟨ _ ⟩} = idp
pointless {y = y}{e ⊙ w} =
begin
(e ⊙ w) ∙w ⟨ y ⟩
≡⟨ idp ⟩
e ⊙ (w ∙w ⟨ y ⟩)
≡⟨ ap (e ⊙_) (pointless {w = w}) ⟩
(e ⊙ w)
∎
walk-respects-∙w' : ∀ {x y z} → (p : Walk' G x y) (q : Walk' G y z)
→ walk (p ·w' q) ≡ (walk p ∙w walk q)
walk-respects-∙w' p ⟨ _ ⟩' = ! pointless
walk-respects-∙w' {z = z} p (q ⊙' x) =
begin
(walk (p ·w' q) ·w (x ⊙ ⟨ z ⟩))
≡⟨ ap (_·w (x ⊙ ⟨ z ⟩)) (walk-respects-∙w' p q) ⟩
((walk p ∙w walk q) ·w (x ⊙ ⟨ z ⟩))
≡⟨ ∙w-assoc (walk p) (walk q) (x ⊙ ⟨ z ⟩) ⟩
((walk p ∙w (walk q ·w (x ⊙ ⟨ z ⟩))))
∎
∙w-assoc' : (w₁ : Walk' G x y)(w₂ : Walk' G y z)(w₃ : Walk' G z w)
→ ((w₁ ·w' w₂) ·w' w₃) ≡ (w₁ ·w' (w₂ ·w' w₃))
∙w-assoc' w₁ w₂ ⟨ _ ⟩' = idp
∙w-assoc' w₁ w₂ (w₃ ⊙' e) = ap (_⊙' e) (∙w-assoc' w₁ w₂ w₃)
pointless' : ∀ {x y} {q : Walk' G x y}
→ (⟨ x ⟩' ·w' q ) ≡ q
pointless' {q = ⟨ _ ⟩'} = idp
pointless' {q = q ⊙' e} = ap (_⊙' e) pointless'
walk'-respects-∙w : ∀ {x y z} → (p : Walk G x y) (q : Walk G y z)
→ walk' (p ·w q) ≡ (walk' p ·w' walk' q)
walk'-respects-∙w ⟨ _ ⟩ q = ! pointless'
walk'-respects-∙w (x ⊙ p) q = ap (λ o → (⟨ _ ⟩' ⊙' x) ·w' o)
(walk'-respects-∙w p q) · ! (∙w-assoc' _ (walk' p) (walk' q))
walk≃walk' : ∀ {x y} → Walk G x y ≃ Walk' G x y
walk≃walk' = qinv-≃ walk' (walk , H1 , H2)
where
private
H1 : ∀ {x y} → (w' : Walk' G x y) → walk' (walk w') ≡ w'
H1 ⟨ _ ⟩' = idp
H1 (w ⊙' e) =
begin
walk' (walk (w ⊙' e))
≡⟨ ap walk' (walk-respects-∙w' w (⟨ _ ⟩' ⊙' e )) ⟩
walk' (walk w ·w (e ⊙ ⟨ _ ⟩))
≡⟨ walk'-respects-∙w (walk w) _ ⟩
(walk' (walk w) ·w' walk' (e ⊙ ⟨ _ ⟩))
≡⟨ ap (_·w' walk' (e ⊙ ⟨ _ ⟩)) (H1 w) ⟩
(w ⊙' e)
∎
H2 : ∀ {x y} → (w' : Walk G x y) → walk (walk' w') ≡ w'
H2 ⟨ _ ⟩ = idp
H2 (e ⊙ w) =
begin
walk ((⟨ _ ⟩' ⊙' e) ·w' walk' w)
≡⟨ walk-respects-∙w' _ (walk' w) ⟩
(walk (⟨ _ ⟩' ⊙' e) ·w (walk (walk' w)))
≡⟨ ap ( e ⊙_) (H2 w) ⟩
(e ⊙ w)
∎
length≡0-is-trivial
: ∀ {a b}
→ (p : Walk G a b)
→ length p ≡ 0
→ ∑[ α ∶ b ≡ a ] ((tr (λ o → Walk G a o) α p) ≡ ⟨ a ⟩)
length≡0-is-trivial ⟨ _ ⟩ idp = (idp , idp)
length≡0-only-same-points
: ∀ {x y} (w : Walk G x y)
→ length w ≡ 0
→ x ≠ y → ⊥ ℓ
length≡0-only-same-points w p x≠y
with length≡0-is-trivial w p
... | idp , idp = ⊥-elim (x≠y idp)
concat-has-positive-len
: ∀ {a b c} (e : Edge G a b)
→ (p : Walk G b c)
→ length (e ⊙ p) ≡ 0
→ ⊥ ℓ
concat-has-positive-len _ ⟨ _ ⟩ ()
concat-has-positive-len _ (x ⊙ p) ()
length>0
: ∀ {a b}
→ (p : Walk G a b)
→ length p < 0
→ ⊥ ℓ
length>0 ⟨ _ ⟩ ()
length>0 (x ⊙ p) ()
length-∙
: ∀ {a b c}
→ (p : Walk G a b) (q : Walk G b c)
→ (length (p ∙w q) > length q)
+ (length (p ∙w q) ≡ length q)
length-∙ ⟨ _ ⟩ q = inr idp
length-∙ (x ⊙ p) q
with length-∙ p q
... | inl q<lenpq = inl (<-trans {x = length q} q<lenpq (<-succ (length (p ∙w q))))
... | inr x₁ = inl (tr (λ p → length q < succ p) (! x₁) (<-succ (length q)))
right-part<whole
: ∀ {a b c}
→ (p : Walk G a c) (q : Walk G a b )(r : Walk G b c)
→ p ≡ (q ·w r)
→ length r < succ (length p)
right-part<whole .r ⟨ _ ⟩ r idp = <-succ (length r)
right-part<whole .(x ⊙ (q ·w r)) (x ⊙ q) r idp
= <-trans {x = length r}
(right-part<whole _ q r idp)
(<-succ (length (q ∙w r)))
left-part<whole
: ∀ {a b c}
→ (p : Walk G a c) (q : Walk G a b )(r : Walk G b c)
→ p ≡ (q ·w r)
→ length q < succ (length p)
left-part<whole .r ⟨ _ ⟩ r idp = ∗
left-part<whole .(x ⊙ (q ·w r)) (x ⊙ q) r idp = left-part<whole _ q r idp
≡-walks-to-∑
: ∀ {x y y' z} {e : Edge G x y} {p : Walk G y z}{e' : Edge G x y'}{q : Walk G y' z}
→ (e ⊙ p) ≡ (e' ⊙ q)
→ ∑[ α ∶ y ≡ y' ] ((tr (λ o → Walk G o z) α p) ≡ q)
≡-walks-to-∑ idp = idp , idp
(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