Walks in directed graphs
module graph-theory.walks-directed-graphs where
Imports
open import elementary-number-theory.natural-numbers open import foundation.cartesian-product-types open import foundation.commuting-squares-of-maps open import foundation.contractible-types open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.functions open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.injective-maps open import foundation.negation open import foundation.raising-universe-levels open import foundation.universe-levels open import graph-theory.directed-graphs open import graph-theory.equivalences-directed-graphs open import graph-theory.morphisms-directed-graphs
Idea
A walk in a directed graph from a vertex x to a vertex y is a list of edges
that connect x to y. Since every journey begins with a single step, we
define the cons operation on walks in directed graphs with an edge from the
source in the first argument, and a walk to the target in the second argument.
Definitions
The type of walks from x to y in G
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) where data walk-Directed-Graph : (x y : vertex-Directed-Graph G) → UU (l1 ⊔ l2) where refl-walk-Directed-Graph : {x : vertex-Directed-Graph G} → walk-Directed-Graph x x cons-walk-Directed-Graph : {x y z : vertex-Directed-Graph G} → edge-Directed-Graph G x y → walk-Directed-Graph y z → walk-Directed-Graph x z unit-walk-Directed-Graph : {x y : vertex-Directed-Graph G} (e : edge-Directed-Graph G x y) → walk-Directed-Graph x y unit-walk-Directed-Graph e = cons-walk-Directed-Graph e refl-walk-Directed-Graph snoc-walk-Directed-Graph : {x y z : vertex-Directed-Graph G} → walk-Directed-Graph x y → edge-Directed-Graph G y z → walk-Directed-Graph x z snoc-walk-Directed-Graph refl-walk-Directed-Graph e = unit-walk-Directed-Graph e snoc-walk-Directed-Graph (cons-walk-Directed-Graph f w) e = cons-walk-Directed-Graph f (snoc-walk-Directed-Graph w e)
The type of walks in a directed graph, defined dually
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) where data walk-Directed-Graph' : (x y : vertex-Directed-Graph G) → UU (l1 ⊔ l2) where refl-walk-Directed-Graph' : {x : vertex-Directed-Graph G} → walk-Directed-Graph' x x snoc-walk-Directed-Graph' : {x y z : vertex-Directed-Graph G} → walk-Directed-Graph' x y → edge-Directed-Graph G y z → walk-Directed-Graph' x z unit-walk-Directed-Graph' : {x y : vertex-Directed-Graph G} → edge-Directed-Graph G x y → walk-Directed-Graph' x y unit-walk-Directed-Graph' e = snoc-walk-Directed-Graph' refl-walk-Directed-Graph' e cons-walk-Directed-Graph' : {x y z : vertex-Directed-Graph G} → edge-Directed-Graph G x y → walk-Directed-Graph' y z → walk-Directed-Graph' x z cons-walk-Directed-Graph' e refl-walk-Directed-Graph' = unit-walk-Directed-Graph' e cons-walk-Directed-Graph' e (snoc-walk-Directed-Graph' w f) = snoc-walk-Directed-Graph' (cons-walk-Directed-Graph' e w) f
The length of a walk in G
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) where length-walk-Directed-Graph : {x y : vertex-Directed-Graph G} → walk-Directed-Graph G x y → ℕ length-walk-Directed-Graph refl-walk-Directed-Graph = 0 length-walk-Directed-Graph (cons-walk-Directed-Graph x w) = succ-ℕ (length-walk-Directed-Graph w)
The type of walks of length n from x to y in G
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) where walk-of-length-Directed-Graph : ℕ → (x y : vertex-Directed-Graph G) → UU (l1 ⊔ l2) walk-of-length-Directed-Graph zero-ℕ x y = raise l2 (y ＝ x) walk-of-length-Directed-Graph (succ-ℕ n) x y = Σ ( vertex-Directed-Graph G) ( λ z → edge-Directed-Graph G x z × walk-of-length-Directed-Graph n z y) map-compute-total-walk-of-length-Directed-Graph : (x y : vertex-Directed-Graph G) → Σ ℕ (λ n → walk-of-length-Directed-Graph n x y) → walk-Directed-Graph G x y map-compute-total-walk-of-length-Directed-Graph x .x (zero-ℕ , map-raise refl) = refl-walk-Directed-Graph map-compute-total-walk-of-length-Directed-Graph x y (succ-ℕ n , z , e , w) = cons-walk-Directed-Graph e ( map-compute-total-walk-of-length-Directed-Graph z y (n , w)) map-inv-compute-total-walk-of-length-Directed-Graph : (x y : vertex-Directed-Graph G) → walk-Directed-Graph G x y → Σ ℕ (λ n → walk-of-length-Directed-Graph n x y) map-inv-compute-total-walk-of-length-Directed-Graph x .x refl-walk-Directed-Graph = (0 , map-raise refl) map-inv-compute-total-walk-of-length-Directed-Graph x y ( cons-walk-Directed-Graph {y = z} e w) = map-Σ ( λ n → walk-of-length-Directed-Graph n x y) ( succ-ℕ) ( λ k u → (z , e , u)) ( map-inv-compute-total-walk-of-length-Directed-Graph z y w) issec-map-inv-compute-total-walk-of-length-Directed-Graph : (x y : vertex-Directed-Graph G) → ( map-compute-total-walk-of-length-Directed-Graph x y ∘ map-inv-compute-total-walk-of-length-Directed-Graph x y) ~ id issec-map-inv-compute-total-walk-of-length-Directed-Graph x .x refl-walk-Directed-Graph = refl issec-map-inv-compute-total-walk-of-length-Directed-Graph x y (cons-walk-Directed-Graph {y = z} e w) = ap ( cons-walk-Directed-Graph e) ( issec-map-inv-compute-total-walk-of-length-Directed-Graph z y w) isretr-map-inv-compute-total-walk-of-length-Directed-Graph : (x y : vertex-Directed-Graph G) → ( map-inv-compute-total-walk-of-length-Directed-Graph x y ∘ map-compute-total-walk-of-length-Directed-Graph x y) ~ id isretr-map-inv-compute-total-walk-of-length-Directed-Graph x .x (zero-ℕ , map-raise refl) = refl isretr-map-inv-compute-total-walk-of-length-Directed-Graph x y (succ-ℕ n , (z , e , w)) = ap ( map-Σ ( λ n → walk-of-length-Directed-Graph n x y) ( succ-ℕ) ( λ k u → (z , e , u))) ( isretr-map-inv-compute-total-walk-of-length-Directed-Graph z y (n , w)) is-equiv-map-compute-total-walk-of-length-Directed-Graph : (x y : vertex-Directed-Graph G) → is-equiv (map-compute-total-walk-of-length-Directed-Graph x y) is-equiv-map-compute-total-walk-of-length-Directed-Graph x y = is-equiv-has-inverse ( map-inv-compute-total-walk-of-length-Directed-Graph x y) ( issec-map-inv-compute-total-walk-of-length-Directed-Graph x y) ( isretr-map-inv-compute-total-walk-of-length-Directed-Graph x y) compute-total-walk-of-length-Directed-Graph : (x y : vertex-Directed-Graph G) → Σ ℕ (λ n → walk-of-length-Directed-Graph n x y) ≃ walk-Directed-Graph G x y pr1 (compute-total-walk-of-length-Directed-Graph x y) = map-compute-total-walk-of-length-Directed-Graph x y pr2 (compute-total-walk-of-length-Directed-Graph x y) = is-equiv-map-compute-total-walk-of-length-Directed-Graph x y
Concatenation of walks
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) where concat-walk-Directed-Graph : {x y z : vertex-Directed-Graph G} → walk-Directed-Graph G x y → walk-Directed-Graph G y z → walk-Directed-Graph G x z concat-walk-Directed-Graph refl-walk-Directed-Graph v = v concat-walk-Directed-Graph (cons-walk-Directed-Graph e u) v = cons-walk-Directed-Graph e (concat-walk-Directed-Graph u v)
Properties
The two dual definitions of walks are equivalent
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) where map-compute-walk-Directed-Graph : {x y : vertex-Directed-Graph G} → walk-Directed-Graph G x y → walk-Directed-Graph' G x y map-compute-walk-Directed-Graph refl-walk-Directed-Graph = refl-walk-Directed-Graph' map-compute-walk-Directed-Graph (cons-walk-Directed-Graph e w) = cons-walk-Directed-Graph' G e (map-compute-walk-Directed-Graph w) compute-snoc-map-compute-walk-Directed-Graph : {x y z : vertex-Directed-Graph G} (w : walk-Directed-Graph G x y) (e : edge-Directed-Graph G y z) → map-compute-walk-Directed-Graph (snoc-walk-Directed-Graph G w e) ＝ snoc-walk-Directed-Graph' (map-compute-walk-Directed-Graph w) e compute-snoc-map-compute-walk-Directed-Graph refl-walk-Directed-Graph e = refl compute-snoc-map-compute-walk-Directed-Graph ( cons-walk-Directed-Graph f w) ( e) = ap ( cons-walk-Directed-Graph' G f) ( compute-snoc-map-compute-walk-Directed-Graph w e) map-inv-compute-walk-Directed-Graph : {x y : vertex-Directed-Graph G} → walk-Directed-Graph' G x y → walk-Directed-Graph G x y map-inv-compute-walk-Directed-Graph refl-walk-Directed-Graph' = refl-walk-Directed-Graph map-inv-compute-walk-Directed-Graph (snoc-walk-Directed-Graph' w e) = snoc-walk-Directed-Graph G (map-inv-compute-walk-Directed-Graph w) e compute-cons-map-inv-compute-walk-Directed-Graph : {x y z : vertex-Directed-Graph G} (e : edge-Directed-Graph G x y) (w : walk-Directed-Graph' G y z) → map-inv-compute-walk-Directed-Graph (cons-walk-Directed-Graph' G e w) ＝ cons-walk-Directed-Graph e (map-inv-compute-walk-Directed-Graph w) compute-cons-map-inv-compute-walk-Directed-Graph e refl-walk-Directed-Graph' = refl compute-cons-map-inv-compute-walk-Directed-Graph e ( snoc-walk-Directed-Graph' w f) = ap ( λ v → snoc-walk-Directed-Graph G v f) ( compute-cons-map-inv-compute-walk-Directed-Graph e w) issec-map-inv-compute-walk-Directed-Graph : {x y : vertex-Directed-Graph G} → ( map-compute-walk-Directed-Graph {x} {y} ∘ map-inv-compute-walk-Directed-Graph {x} {y}) ~ id issec-map-inv-compute-walk-Directed-Graph refl-walk-Directed-Graph' = refl issec-map-inv-compute-walk-Directed-Graph (snoc-walk-Directed-Graph' w e) = ( compute-snoc-map-compute-walk-Directed-Graph ( map-inv-compute-walk-Directed-Graph w) ( e)) ∙ ( ap ( λ v → snoc-walk-Directed-Graph' v e) ( issec-map-inv-compute-walk-Directed-Graph w)) isretr-map-inv-compute-walk-Directed-Graph : {x y : vertex-Directed-Graph G} → ( map-inv-compute-walk-Directed-Graph {x} {y} ∘ map-compute-walk-Directed-Graph {x} {y}) ~ id isretr-map-inv-compute-walk-Directed-Graph refl-walk-Directed-Graph = refl isretr-map-inv-compute-walk-Directed-Graph (cons-walk-Directed-Graph e w) = ( compute-cons-map-inv-compute-walk-Directed-Graph e ( map-compute-walk-Directed-Graph w)) ∙ ( ap ( cons-walk-Directed-Graph e) ( isretr-map-inv-compute-walk-Directed-Graph w)) is-equiv-map-compute-walk-Directed-Graph : {x y : vertex-Directed-Graph G} → is-equiv (map-compute-walk-Directed-Graph {x} {y}) is-equiv-map-compute-walk-Directed-Graph = is-equiv-has-inverse map-inv-compute-walk-Directed-Graph issec-map-inv-compute-walk-Directed-Graph isretr-map-inv-compute-walk-Directed-Graph compute-walk-Directed-Graph : (x y : vertex-Directed-Graph G) → walk-Directed-Graph G x y ≃ walk-Directed-Graph' G x y pr1 (compute-walk-Directed-Graph x y) = map-compute-walk-Directed-Graph pr2 (compute-walk-Directed-Graph x y) = is-equiv-map-compute-walk-Directed-Graph
The type of walks from x to y is a coproduct
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) where coproduct-walk-Directed-Graph : (x y : vertex-Directed-Graph G) → UU (l1 ⊔ l2) coproduct-walk-Directed-Graph x y = (y ＝ x) + Σ ( vertex-Directed-Graph G) ( λ z → edge-Directed-Graph G x z × walk-Directed-Graph G z y) map-compute-coproduct-walk-Directed-Graph : (x y : vertex-Directed-Graph G) → walk-Directed-Graph G x y → coproduct-walk-Directed-Graph x y map-compute-coproduct-walk-Directed-Graph x .x refl-walk-Directed-Graph = inl refl map-compute-coproduct-walk-Directed-Graph x y ( cons-walk-Directed-Graph {a} {b} {c} e w) = inr (b , e , w) map-inv-compute-coproduct-walk-Directed-Graph : (x y : vertex-Directed-Graph G) → coproduct-walk-Directed-Graph x y → walk-Directed-Graph G x y map-inv-compute-coproduct-walk-Directed-Graph x .x (inl refl) = refl-walk-Directed-Graph map-inv-compute-coproduct-walk-Directed-Graph x y (inr (z , e , w)) = cons-walk-Directed-Graph e w issec-map-inv-compute-coproduct-walk-Directed-Graph : (x y : vertex-Directed-Graph G) → ( map-compute-coproduct-walk-Directed-Graph x y ∘ map-inv-compute-coproduct-walk-Directed-Graph x y) ~ id issec-map-inv-compute-coproduct-walk-Directed-Graph x .x (inl refl) = refl issec-map-inv-compute-coproduct-walk-Directed-Graph x y (inr (z , e , w)) = refl isretr-map-inv-compute-coproduct-walk-Directed-Graph : (x y : vertex-Directed-Graph G) → ( map-inv-compute-coproduct-walk-Directed-Graph x y ∘ map-compute-coproduct-walk-Directed-Graph x y) ~ id isretr-map-inv-compute-coproduct-walk-Directed-Graph x .x refl-walk-Directed-Graph = refl isretr-map-inv-compute-coproduct-walk-Directed-Graph x y ( cons-walk-Directed-Graph e w) = refl is-equiv-map-compute-coproduct-walk-Directed-Graph : (x y : vertex-Directed-Graph G) → is-equiv (map-compute-coproduct-walk-Directed-Graph x y) is-equiv-map-compute-coproduct-walk-Directed-Graph x y = is-equiv-has-inverse ( map-inv-compute-coproduct-walk-Directed-Graph x y) ( issec-map-inv-compute-coproduct-walk-Directed-Graph x y) ( isretr-map-inv-compute-coproduct-walk-Directed-Graph x y) compute-coproduct-walk-Directed-Graph : (x y : vertex-Directed-Graph G) → walk-Directed-Graph G x y ≃ coproduct-walk-Directed-Graph x y pr1 (compute-coproduct-walk-Directed-Graph x y) = map-compute-coproduct-walk-Directed-Graph x y pr2 (compute-coproduct-walk-Directed-Graph x y) = is-equiv-map-compute-coproduct-walk-Directed-Graph x y
Walks of length 0 are identifications
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) (x : vertex-Directed-Graph G) where is-contr-total-walk-of-length-zero-Directed-Graph : is-contr ( Σ ( vertex-Directed-Graph G) ( λ y → walk-of-length-Directed-Graph G 0 x y)) is-contr-total-walk-of-length-zero-Directed-Graph = is-contr-equiv' ( Σ (vertex-Directed-Graph G) (λ y → y ＝ x)) ( equiv-tot (λ y → compute-raise l2 (y ＝ x))) ( is-contr-total-path' x)
cons-walk e w ≠ refl-walk
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) (x : vertex-Directed-Graph G) where neq-cons-refl-walk-Directed-Graph : (y : vertex-Directed-Graph G) (e : edge-Directed-Graph G x y) → (w : walk-Directed-Graph G y x) → ¬ (cons-walk-Directed-Graph e w ＝ refl-walk-Directed-Graph) neq-cons-refl-walk-Directed-Graph y e w ()
If cons-walk e w ＝ cons-walk e' w', then (y , e) ＝ (y' , e')
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) (x : vertex-Directed-Graph G) where eq-direct-successor-eq-cons-walk-Directed-Graph : {y y' z : vertex-Directed-Graph G} (e : edge-Directed-Graph G x y) (e' : edge-Directed-Graph G x y') (w : walk-Directed-Graph G y z) (w' : walk-Directed-Graph G y' z) → cons-walk-Directed-Graph e w ＝ cons-walk-Directed-Graph e' w' → (y , e) ＝ (y' , e') eq-direct-successor-eq-cons-walk-Directed-Graph {y} {.y} {z} e .e w .w refl = refl
Vertices on a walk
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) where is-vertex-on-walk-Directed-Graph : {x y : vertex-Directed-Graph G} (w : walk-Directed-Graph G x y) (v : vertex-Directed-Graph G) → UU l1 is-vertex-on-walk-Directed-Graph {x} refl-walk-Directed-Graph v = v ＝ x is-vertex-on-walk-Directed-Graph {x} (cons-walk-Directed-Graph e w) v = ( v ＝ x) + ( is-vertex-on-walk-Directed-Graph w v) vertex-on-walk-Directed-Graph : {x y : vertex-Directed-Graph G} (w : walk-Directed-Graph G x y) → UU l1 vertex-on-walk-Directed-Graph w = Σ (vertex-Directed-Graph G) (is-vertex-on-walk-Directed-Graph w) vertex-vertex-on-walk-Directed-Graph : {x y : vertex-Directed-Graph G} (w : walk-Directed-Graph G x y) → vertex-on-walk-Directed-Graph w → vertex-Directed-Graph G vertex-vertex-on-walk-Directed-Graph w = pr1
Edges on a walk
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) where data is-edge-on-walk-Directed-Graph : {x y : vertex-Directed-Graph G} (w : walk-Directed-Graph G x y) {u v : vertex-Directed-Graph G} → edge-Directed-Graph G u v → UU (l1 ⊔ l2) where edge-is-edge-on-walk-Directed-Graph : {x y z : vertex-Directed-Graph G} (e : edge-Directed-Graph G x y) (w : walk-Directed-Graph G y z) → is-edge-on-walk-Directed-Graph (cons-walk-Directed-Graph e w) e cons-is-edge-on-walk-Directed-Graph : {x y z : vertex-Directed-Graph G} (e : edge-Directed-Graph G x y) (w : walk-Directed-Graph G y z) → {u v : vertex-Directed-Graph G} (f : edge-Directed-Graph G u v) → is-edge-on-walk-Directed-Graph w f → is-edge-on-walk-Directed-Graph (cons-walk-Directed-Graph e w) f edge-on-walk-Directed-Graph : {x y : vertex-Directed-Graph G} (w : walk-Directed-Graph G x y) → UU (l1 ⊔ l2) edge-on-walk-Directed-Graph w = Σ ( total-edge-Directed-Graph G) ( λ e → is-edge-on-walk-Directed-Graph w (edge-total-edge-Directed-Graph G e)) module _ {x y : vertex-Directed-Graph G} (w : walk-Directed-Graph G x y) (e : edge-on-walk-Directed-Graph w) where total-edge-edge-on-walk-Directed-Graph : total-edge-Directed-Graph G total-edge-edge-on-walk-Directed-Graph = pr1 e source-edge-on-walk-Directed-Graph : vertex-Directed-Graph G source-edge-on-walk-Directed-Graph = source-total-edge-Directed-Graph G total-edge-edge-on-walk-Directed-Graph target-edge-on-walk-Directed-Graph : vertex-Directed-Graph G target-edge-on-walk-Directed-Graph = target-total-edge-Directed-Graph G total-edge-edge-on-walk-Directed-Graph edge-edge-on-walk-Directed-Graph : edge-Directed-Graph G source-edge-on-walk-Directed-Graph target-edge-on-walk-Directed-Graph edge-edge-on-walk-Directed-Graph = edge-total-edge-Directed-Graph G total-edge-edge-on-walk-Directed-Graph is-edge-on-walk-edge-on-walk-Directed-Graph : is-edge-on-walk-Directed-Graph w edge-edge-on-walk-Directed-Graph is-edge-on-walk-edge-on-walk-Directed-Graph = pr2 e
The action on walks of graph homomorphisms
walk-hom-Directed-Graph : {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4) (f : hom-Directed-Graph G H) {x y : vertex-Directed-Graph G} → walk-Directed-Graph G x y → walk-Directed-Graph H ( vertex-hom-Directed-Graph G H f x) ( vertex-hom-Directed-Graph G H f y) walk-hom-Directed-Graph G H f refl-walk-Directed-Graph = refl-walk-Directed-Graph walk-hom-Directed-Graph G H f (cons-walk-Directed-Graph e w) = cons-walk-Directed-Graph ( edge-hom-Directed-Graph G H f e) ( walk-hom-Directed-Graph G H f w)
The action on walks of length n of graph homomorphisms
module _ {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4) (f : hom-Directed-Graph G H) where walk-of-length-hom-Directed-Graph : (n : ℕ) {x y : vertex-Directed-Graph G} → walk-of-length-Directed-Graph G n x y → walk-of-length-Directed-Graph H n ( vertex-hom-Directed-Graph G H f x) ( vertex-hom-Directed-Graph G H f y) walk-of-length-hom-Directed-Graph zero-ℕ {x} {y} (map-raise p) = map-raise (ap (vertex-hom-Directed-Graph G H f) p) walk-of-length-hom-Directed-Graph (succ-ℕ n) = map-Σ ( λ z → ( edge-Directed-Graph H (vertex-hom-Directed-Graph G H f _) z) × ( walk-of-length-Directed-Graph H n z ( vertex-hom-Directed-Graph G H f _))) ( vertex-hom-Directed-Graph G H f) ( λ z → map-prod ( edge-hom-Directed-Graph G H f) ( walk-of-length-hom-Directed-Graph n)) square-compute-total-walk-of-length-hom-Directed-Graph : (x y : vertex-Directed-Graph G) → coherence-square-maps ( tot (λ n → walk-of-length-hom-Directed-Graph n {x} {y})) ( map-compute-total-walk-of-length-Directed-Graph G x y) ( map-compute-total-walk-of-length-Directed-Graph H ( vertex-hom-Directed-Graph G H f x) ( vertex-hom-Directed-Graph G H f y)) ( walk-hom-Directed-Graph G H f {x} {y}) square-compute-total-walk-of-length-hom-Directed-Graph x .x (zero-ℕ , map-raise refl) = refl square-compute-total-walk-of-length-hom-Directed-Graph x y (succ-ℕ n , z , e , w) = ap ( cons-walk-Directed-Graph (edge-hom-Directed-Graph G H f e)) ( square-compute-total-walk-of-length-hom-Directed-Graph z y (n , w))
The action on walks of length n of equivalences of graphs
equiv-walk-of-length-equiv-Directed-Graph : {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4) (f : equiv-Directed-Graph G H) (n : ℕ) {x y : vertex-Directed-Graph G} → walk-of-length-Directed-Graph G n x y ≃ walk-of-length-Directed-Graph H n ( vertex-equiv-Directed-Graph G H f x) ( vertex-equiv-Directed-Graph G H f y) equiv-walk-of-length-equiv-Directed-Graph G H f zero-ℕ = equiv-raise _ _ ( equiv-ap (equiv-vertex-equiv-Directed-Graph G H f) _ _) equiv-walk-of-length-equiv-Directed-Graph G H f (succ-ℕ n) = equiv-Σ ( λ z → ( edge-Directed-Graph H (vertex-equiv-Directed-Graph G H f _) z) × ( walk-of-length-Directed-Graph H n z ( vertex-equiv-Directed-Graph G H f _))) ( equiv-vertex-equiv-Directed-Graph G H f) ( λ z → equiv-prod ( equiv-edge-equiv-Directed-Graph G H f _ _) ( equiv-walk-of-length-equiv-Directed-Graph G H f n))
The action of equivalences on walks
module _ {l1 l2 l3 l4 : Level} (G : Directed-Graph l1 l2) (H : Directed-Graph l3 l4) (e : equiv-Directed-Graph G H) where walk-equiv-Directed-Graph : {x y : vertex-Directed-Graph G} → walk-Directed-Graph G x y → walk-Directed-Graph H ( vertex-equiv-Directed-Graph G H e x) ( vertex-equiv-Directed-Graph G H e y) walk-equiv-Directed-Graph = walk-hom-Directed-Graph G H (hom-equiv-Directed-Graph G H e) square-compute-total-walk-of-length-equiv-Directed-Graph : (x y : vertex-Directed-Graph G) → coherence-square-maps ( tot ( λ n → map-equiv ( equiv-walk-of-length-equiv-Directed-Graph G H e n {x} {y}))) ( map-compute-total-walk-of-length-Directed-Graph G x y) ( map-compute-total-walk-of-length-Directed-Graph H ( vertex-equiv-Directed-Graph G H e x) ( vertex-equiv-Directed-Graph G H e y)) ( walk-equiv-Directed-Graph {x} {y}) square-compute-total-walk-of-length-equiv-Directed-Graph x .x (zero-ℕ , map-raise refl) = refl square-compute-total-walk-of-length-equiv-Directed-Graph x y (succ-ℕ n , z , f , w) = ap ( cons-walk-Directed-Graph (edge-equiv-Directed-Graph G H e x z f)) ( square-compute-total-walk-of-length-equiv-Directed-Graph z y (n , w)) is-equiv-walk-equiv-Directed-Graph : {x y : vertex-Directed-Graph G} → is-equiv (walk-equiv-Directed-Graph {x} {y}) is-equiv-walk-equiv-Directed-Graph {x} {y} = is-equiv-right-is-equiv-left-square ( map-equiv ( equiv-tot ( λ n → equiv-walk-of-length-equiv-Directed-Graph G H e n {x} {y}))) ( walk-equiv-Directed-Graph {x} {y}) ( map-compute-total-walk-of-length-Directed-Graph G x y) ( map-compute-total-walk-of-length-Directed-Graph H ( vertex-equiv-Directed-Graph G H e x) ( vertex-equiv-Directed-Graph G H e y)) ( inv-htpy ( square-compute-total-walk-of-length-equiv-Directed-Graph x y)) ( is-equiv-map-compute-total-walk-of-length-Directed-Graph G x y) ( is-equiv-map-compute-total-walk-of-length-Directed-Graph H ( vertex-equiv-Directed-Graph G H e x) ( vertex-equiv-Directed-Graph G H e y)) ( is-equiv-map-equiv ( equiv-tot ( λ n → equiv-walk-of-length-equiv-Directed-Graph G H e n))) equiv-walk-equiv-Directed-Graph : {x y : vertex-Directed-Graph G} → walk-Directed-Graph G x y ≃ walk-Directed-Graph H ( vertex-equiv-Directed-Graph G H e x) ( vertex-equiv-Directed-Graph G H e y) pr1 (equiv-walk-equiv-Directed-Graph {x} {y}) = walk-equiv-Directed-Graph pr2 (equiv-walk-equiv-Directed-Graph {x} {y}) = is-equiv-walk-equiv-Directed-Graph
If concat-walk-Directed-Graph u v ＝ refl-walk-Directed-Graph then both u and v are refl-walk-Directed-Graph
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) where eq-is-refl-concat-walk-Directed-Graph : {x y : vertex-Directed-Graph G} → (u : walk-Directed-Graph G x y) (v : walk-Directed-Graph G y x) → ( concat-walk-Directed-Graph G u v ＝ refl-walk-Directed-Graph) → x ＝ y eq-is-refl-concat-walk-Directed-Graph refl-walk-Directed-Graph .refl-walk-Directed-Graph refl = refl is-refl-left-is-refl-concat-walk-Directed-Graph : {x y : vertex-Directed-Graph G} (u : walk-Directed-Graph G x y) (v : walk-Directed-Graph G y x) → (p : concat-walk-Directed-Graph G u v ＝ refl-walk-Directed-Graph) → tr ( walk-Directed-Graph G x) ( eq-is-refl-concat-walk-Directed-Graph u v p) ( refl-walk-Directed-Graph) ＝ u is-refl-left-is-refl-concat-walk-Directed-Graph refl-walk-Directed-Graph .refl-walk-Directed-Graph refl = refl is-refl-right-is-refl-concat-walk-Directed-Graph : {x y : vertex-Directed-Graph G} (u : walk-Directed-Graph G x y) (v : walk-Directed-Graph G y x) → (p : concat-walk-Directed-Graph G u v ＝ refl-walk-Directed-Graph) → tr ( walk-Directed-Graph G y) ( inv (eq-is-refl-concat-walk-Directed-Graph u v p)) ( refl-walk-Directed-Graph) ＝ v is-refl-right-is-refl-concat-walk-Directed-Graph refl-walk-Directed-Graph .refl-walk-Directed-Graph refl = refl
The function unit-walk is injective
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) where is-injective-unit-walk-Directed-Graph : {x y : vertex-Directed-Graph G} → is-injective (unit-walk-Directed-Graph G {x} {y}) is-injective-unit-walk-Directed-Graph refl = refl
The last edge on a walk
module _ {l1 l2 : Level} (G : Directed-Graph l1 l2) where last-stage-walk-Directed-Graph : {x y z : vertex-Directed-Graph G} (e : edge-Directed-Graph G x y) → walk-Directed-Graph G y z → Σ (vertex-Directed-Graph G) (λ u → edge-Directed-Graph G u z) last-stage-walk-Directed-Graph e refl-walk-Directed-Graph = (_ , e) last-stage-walk-Directed-Graph e (cons-walk-Directed-Graph f w) = last-stage-walk-Directed-Graph f w vertex-last-stage-walk-Directed-Graph : {x y z : vertex-Directed-Graph G} (e : edge-Directed-Graph G x y) → walk-Directed-Graph G y z → vertex-Directed-Graph G vertex-last-stage-walk-Directed-Graph e w = pr1 (last-stage-walk-Directed-Graph e w) edge-last-stage-walk-Directed-Graph : {x y z : vertex-Directed-Graph G} (e : edge-Directed-Graph G x y) → (w : walk-Directed-Graph G y z) → edge-Directed-Graph G (vertex-last-stage-walk-Directed-Graph e w) z edge-last-stage-walk-Directed-Graph e w = pr2 (last-stage-walk-Directed-Graph e w) walk-last-stage-walk-Directed-Graph : {x y z : vertex-Directed-Graph G} (e : edge-Directed-Graph G x y) → (w : walk-Directed-Graph G y z) → walk-Directed-Graph G x (vertex-last-stage-walk-Directed-Graph e w) walk-last-stage-walk-Directed-Graph e refl-walk-Directed-Graph = refl-walk-Directed-Graph walk-last-stage-walk-Directed-Graph e (cons-walk-Directed-Graph f w) = cons-walk-Directed-Graph e (walk-last-stage-walk-Directed-Graph f w)