The underlying trees of elements of W-types
module trees.underlying-trees-of-elements-of-w-types where
Imports
open import foundation.contractible-types open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.equivalence-extensionality open import foundation.equivalences open import foundation.functions open import foundation.homotopies open import foundation.identity-types open import foundation.isolated-points open import foundation.negation open import foundation.propositions open import foundation.universe-levels open import graph-theory.directed-graphs open import graph-theory.morphisms-directed-graphs open import graph-theory.walks-directed-graphs open import trees.combinator-directed-trees open import trees.combinator-enriched-directed-trees open import trees.directed-trees open import trees.elementhood-relation-w-types open import trees.enriched-directed-trees open import trees.equivalences-directed-trees open import trees.equivalences-enriched-directed-trees open import trees.underlying-trees-elements-coalgebras-polynomial-endofunctors open import trees.w-types
Idea
The underlying (enriched) directed tree of an element of a W-type is the
underlying (enriched) directed tree of that element obtained via the coalgebra
structure of 𝕎 A B.
Definitions
The underlying enriched directed tree of an element of a W-type
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where enriched-directed-tree-element-𝕎 : 𝕎 A B → Enriched-Directed-Tree (l1 ⊔ l2) (l1 ⊔ l2) A B enriched-directed-tree-element-𝕎 = enriched-directed-tree-element-coalgebra (𝕎-Coalg A B)
The underlying graph of an element of a W-type
graph-element-𝕎 : 𝕎 A B → Directed-Graph (l1 ⊔ l2) (l1 ⊔ l2) graph-element-𝕎 = graph-element-coalgebra (𝕎-Coalg A B) external-graph-element-𝕎 : 𝕎 A B → Directed-Graph (l1 ⊔ l2) (l1 ⊔ l2) external-graph-element-𝕎 = external-graph-element-coalgebra (𝕎-Coalg A B) node-external-graph-element-𝕎 : 𝕎 A B → UU (l1 ⊔ l2) node-external-graph-element-𝕎 = node-external-graph-element-coalgebra (𝕎-Coalg A B) edge-external-graph-element-𝕎 : (w : 𝕎 A B) (x y : node-external-graph-element-𝕎 w) → UU (l1 ⊔ l2) edge-external-graph-element-𝕎 = edge-external-graph-element-coalgebra (𝕎-Coalg A B) inclusion-graph-element-𝕎 : {u v : 𝕎 A B} → u ∈-𝕎 v → hom-Directed-Graph (graph-element-𝕎 u) (graph-element-𝕎 v) inclusion-graph-element-𝕎 = inclusion-element-coalgebra (𝕎-Coalg A B)
Nodes of the underlying directed tree of an element of a W-type
node-element-𝕎 : 𝕎 A B → UU (l1 ⊔ l2) node-element-𝕎 = node-element-coalgebra (𝕎-Coalg A B) node-inclusion-element-𝕎 : {u v : 𝕎 A B} → (u ∈-𝕎 v) → node-element-𝕎 u → node-element-𝕎 v node-inclusion-element-𝕎 = node-inclusion-element-coalgebra
The root of the underlying directed tree of an element of a W-type
root-𝕎 : (w : 𝕎 A B) → node-element-𝕎 w root-𝕎 = root-coalgebra is-root-node-element-𝕎 : (w : 𝕎 A B) (x : node-element-𝕎 w) → UU (l1 ⊔ l2) is-root-node-element-𝕎 = is-root-element-coalgebra (𝕎-Coalg A B) is-isolated-root-element-𝕎 : (w : 𝕎 A B) → is-isolated (root-𝕎 w) is-isolated-root-element-𝕎 = is-isolated-root-element-coalgebra (𝕎-Coalg A B) is-contr-loop-space-root-graph-element-𝕎 : (w : 𝕎 A B) → is-contr (root-𝕎 w ＝ root-𝕎 w) is-contr-loop-space-root-graph-element-𝕎 = is-contr-loop-space-root-element-coalgebra (𝕎-Coalg A B)
The edges of the underlying directed tree of an element of a W-type
edge-element-𝕎 : (w : 𝕎 A B) (x y : node-element-𝕎 w) → UU (l1 ⊔ l2) edge-element-𝕎 = edge-element-coalgebra (𝕎-Coalg A B) edge-to-root-element-𝕎 : {u v : 𝕎 A B} (H : u ∈-𝕎 v) → edge-element-𝕎 v ( node-inclusion-element-𝕎 H (root-𝕎 u)) ( root-𝕎 v) edge-to-root-element-𝕎 = edge-to-root-element-coalgebra edge-inclusion-element-𝕎 : {u v : 𝕎 A B} (H : u ∈-𝕎 v) → {x y : node-element-𝕎 u} (e : edge-element-𝕎 u x y) → edge-element-𝕎 v ( node-inclusion-element-𝕎 H x) ( node-inclusion-element-𝕎 H y) edge-inclusion-element-𝕎 = edge-inclusion-element-coalgebra is-contr-edge-to-root-element-𝕎 : {u v : 𝕎 A B} (H : u ∈-𝕎 v) → is-contr ( edge-element-𝕎 v ( node-inclusion-element-𝕎 H (root-𝕎 u)) ( root-𝕎 v)) is-contr-edge-to-root-element-𝕎 = is-contr-edge-to-root-element-coalgebra (𝕎-Coalg A B) is-proof-irrelevant-edge-to-root-element-𝕎 : (w : 𝕎 A B) (x : node-element-𝕎 w) → is-proof-irrelevant (edge-element-𝕎 w x (root-𝕎 w)) is-proof-irrelevant-edge-to-root-element-𝕎 = is-proof-irrelevant-edge-to-root-element-coalgebra (𝕎-Coalg A B) is-prop-edge-to-root-element-𝕎 : (w : 𝕎 A B) (x : node-element-𝕎 w) → is-prop (edge-element-𝕎 w x (root-𝕎 w)) is-prop-edge-to-root-element-𝕎 = is-prop-edge-to-root-element-coalgebra (𝕎-Coalg A B) no-edge-from-root-graph-element-𝕎 : (w : 𝕎 A B) → is-empty (Σ (node-element-𝕎 w) (edge-element-𝕎 w (root-𝕎 w))) no-edge-from-root-graph-element-𝕎 = no-edge-from-root-element-coalgebra (𝕎-Coalg A B) is-empty-eq-root-node-inclusion-element-𝕎 : {v w : 𝕎 A B} (H : v ∈-𝕎 w) (x : node-element-𝕎 v) → ¬ (root-𝕎 w ＝ node-inclusion-element-𝕎 H x) is-empty-eq-root-node-inclusion-element-𝕎 = is-empty-eq-root-node-inclusion-element-coalgebra (𝕎-Coalg A B)
The underlying directed tree of an element of a W-type
directed-tree-element-𝕎 : 𝕎 A B → Directed-Tree (l1 ⊔ l2) (l1 ⊔ l2) directed-tree-element-𝕎 = directed-tree-element-coalgebra (𝕎-Coalg A B) has-unique-predecessor-node-inclusion-element-𝕎 : {v w : 𝕎 A B} (H : v ∈-𝕎 w) (x : node-element-𝕎 v) → is-contr ( Σ ( node-element-𝕎 w) ( edge-element-𝕎 w (node-inclusion-element-𝕎 H x))) has-unique-predecessor-node-inclusion-element-𝕎 = has-unique-predecessor-node-inclusion-element-coalgebra (𝕎-Coalg A B) has-unique-predecessor-graph-element-𝕎 : (w : 𝕎 A B) (x : node-element-𝕎 w) → is-contr ((root-𝕎 w ＝ x) + Σ (node-element-𝕎 w) (edge-element-𝕎 w x)) has-unique-predecessor-graph-element-𝕎 = has-unique-predecessor-element-coalgebra (𝕎-Coalg A B) walk-to-root-graph-element-𝕎 : (w : 𝕎 A B) (x : node-element-𝕎 w) → walk-Directed-Graph (graph-element-𝕎 w) x (root-𝕎 w) walk-to-root-graph-element-𝕎 = walk-to-root-element-coalgebra (𝕎-Coalg A B) unique-walk-to-root-element-𝕎 : (w : 𝕎 A B) → is-tree-Directed-Graph' (graph-element-𝕎 w) (root-𝕎 w) unique-walk-to-root-element-𝕎 = unique-walk-to-root-element-coalgebra (𝕎-Coalg A B)
The underlying directed tree of an element of a W-type is enriched
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where shape-element-𝕎 : (w : 𝕎 A B) → node-element-𝕎 w → A shape-element-𝕎 = shape-element-coalgebra (𝕎-Coalg A B) map-enrichment-element-𝕎 : (w : 𝕎 A B) (x : node-element-𝕎 w) → B (shape-element-𝕎 w x) → Σ (node-element-𝕎 w) (λ y → edge-element-𝕎 w y x) map-enrichment-element-𝕎 = map-enrichment-element-coalgebra (𝕎-Coalg A B) map-inv-enrichment-element-𝕎 : (w : 𝕎 A B) (x : node-element-𝕎 w) → Σ (node-element-𝕎 w) (λ y → edge-element-𝕎 w y x) → B (shape-element-𝕎 w x) map-inv-enrichment-element-𝕎 = map-inv-enrichment-directed-tree-element-coalgebra (𝕎-Coalg A B) issec-map-inv-enrichment-element-𝕎 : (w : 𝕎 A B) (x : node-element-𝕎 w) → ( map-enrichment-element-𝕎 w x ∘ map-inv-enrichment-element-𝕎 w x) ~ id issec-map-inv-enrichment-element-𝕎 = issec-map-inv-enrichment-directed-tree-element-coalgebra (𝕎-Coalg A B) isretr-map-inv-enrichment-element-𝕎 : (w : 𝕎 A B) (x : node-element-𝕎 w) → ( map-inv-enrichment-element-𝕎 w x ∘ map-enrichment-element-𝕎 w x) ~ id isretr-map-inv-enrichment-element-𝕎 = isretr-map-inv-enrichment-directed-tree-element-coalgebra (𝕎-Coalg A B) is-equiv-map-enrichment-element-𝕎 : (w : 𝕎 A B) (x : node-element-𝕎 w) → is-equiv (map-enrichment-element-𝕎 w x) is-equiv-map-enrichment-element-𝕎 = is-equiv-map-enrichment-element-coalgebra (𝕎-Coalg A B) enrichment-element-𝕎 : (w : 𝕎 A B) (x : node-element-𝕎 w) → B (shape-element-𝕎 w x) ≃ Σ (node-element-𝕎 w) (λ y → edge-element-𝕎 w y x) enrichment-element-𝕎 = enrichment-directed-tree-element-coalgebra (𝕎-Coalg A B)
Properties
Characterization of equality of the type of nodes of the underlying graph of an element of 𝕎 A B
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where Eq-node-element-𝕎 : (w : 𝕎 A B) (x y : node-element-𝕎 w) → UU (l1 ⊔ l2) Eq-node-element-𝕎 = Eq-node-element-coalgebra (𝕎-Coalg A B) root-refl-Eq-node-element-𝕎 : (w : 𝕎 A B) → Eq-node-element-𝕎 w (root-𝕎 w) (root-𝕎 w) root-refl-Eq-node-element-𝕎 w = root-refl-Eq-node-element-coalgebra node-inclusion-Eq-node-element-𝕎 : (w : 𝕎 A B) {u : 𝕎 A B} (H : u ∈-𝕎 w) {x y : node-element-𝕎 u} → Eq-node-element-𝕎 u x y → Eq-node-element-𝕎 w ( node-inclusion-element-𝕎 H x) ( node-inclusion-element-𝕎 H y) node-inclusion-Eq-node-element-𝕎 w = node-inclusion-Eq-node-element-coalgebra refl-Eq-node-element-𝕎 : {w : 𝕎 A B} (x : node-element-𝕎 w) → Eq-node-element-𝕎 w x x refl-Eq-node-element-𝕎 = refl-Eq-node-element-coalgebra (𝕎-Coalg A B) is-contr-total-Eq-node-element-𝕎 : (w : 𝕎 A B) (x : node-element-𝕎 w) → is-contr (Σ (node-element-𝕎 w) (Eq-node-element-𝕎 w x)) is-contr-total-Eq-node-element-𝕎 = is-contr-total-Eq-node-element-coalgebra (𝕎-Coalg A B) Eq-eq-node-element-𝕎 : (w : 𝕎 A B) {x y : node-element-𝕎 w} → x ＝ y → Eq-node-element-𝕎 w x y Eq-eq-node-element-𝕎 = Eq-eq-node-element-coalgebra (𝕎-Coalg A B) is-equiv-Eq-eq-node-element-𝕎 : (w : 𝕎 A B) (x y : node-element-𝕎 w) → is-equiv (Eq-eq-node-element-𝕎 w {x} {y}) is-equiv-Eq-eq-node-element-𝕎 = is-equiv-Eq-eq-node-element-coalgebra (𝕎-Coalg A B) extensionality-node-element-𝕎 : (w : 𝕎 A B) (x y : node-element-𝕎 w) → (x ＝ y) ≃ Eq-node-element-𝕎 w x y extensionality-node-element-𝕎 = extensionality-node-element-coalgebra (𝕎-Coalg A B) eq-Eq-node-element-𝕎 : (w : 𝕎 A B) (x y : node-element-𝕎 w) → Eq-node-element-𝕎 w x y → x ＝ y eq-Eq-node-element-𝕎 = eq-Eq-node-element-coalgebra (𝕎-Coalg A B)
The underlying tree of tree-𝕎 a α is the combinator tree of the underlying trees of α b indexed by b : B a
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (w : 𝕎 A B) where node-compute-directed-tree-element-𝕎 : node-element-𝕎 w → node-combinator-Directed-Tree ( λ b → directed-tree-element-𝕎 (component-𝕎 w b)) node-compute-directed-tree-element-𝕎 = node-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w map-inv-node-compute-directed-tree-element-𝕎 : node-combinator-Directed-Tree ( λ b → directed-tree-element-𝕎 (component-𝕎 w b)) → node-element-𝕎 w map-inv-node-compute-directed-tree-element-𝕎 = map-inv-node-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w issec-map-inv-node-compute-directed-tree-element-𝕎 : ( node-compute-directed-tree-element-𝕎 ∘ map-inv-node-compute-directed-tree-element-𝕎) ~ id issec-map-inv-node-compute-directed-tree-element-𝕎 = issec-map-inv-node-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w isretr-map-inv-node-compute-directed-tree-element-𝕎 : ( map-inv-node-compute-directed-tree-element-𝕎 ∘ node-compute-directed-tree-element-𝕎) ~ id isretr-map-inv-node-compute-directed-tree-element-𝕎 = isretr-map-inv-node-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w is-equiv-node-compute-directed-tree-element-𝕎 : is-equiv node-compute-directed-tree-element-𝕎 is-equiv-node-compute-directed-tree-element-𝕎 = is-equiv-node-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w equiv-node-compute-directed-tree-element-𝕎 : node-element-𝕎 w ≃ node-combinator-Directed-Tree ( λ b → directed-tree-element-𝕎 (component-𝕎 w b)) equiv-node-compute-directed-tree-element-𝕎 = equiv-node-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w edge-compute-directed-tree-element-𝕎 : (x y : node-element-𝕎 w) → edge-element-𝕎 w x y → edge-combinator-Directed-Tree ( λ b → directed-tree-element-𝕎 (component-𝕎 w b)) ( node-compute-directed-tree-element-𝕎 x) ( node-compute-directed-tree-element-𝕎 y) edge-compute-directed-tree-element-𝕎 = edge-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w map-inv-edge-compute-directed-tree-element-𝕎 : ( x y : node-element-𝕎 w) → edge-combinator-Directed-Tree ( λ b → directed-tree-element-𝕎 (component-𝕎 w b)) ( node-compute-directed-tree-element-𝕎 x) ( node-compute-directed-tree-element-𝕎 y) → edge-element-𝕎 w x y map-inv-edge-compute-directed-tree-element-𝕎 = map-inv-edge-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w issec-map-inv-edge-compute-directed-tree-element-𝕎 : (x y : node-element-𝕎 w) → ( e : edge-combinator-Directed-Tree ( λ b → directed-tree-element-𝕎 (component-𝕎 w b)) ( node-compute-directed-tree-element-𝕎 x) ( node-compute-directed-tree-element-𝕎 y)) → edge-compute-directed-tree-element-𝕎 x y ( map-inv-edge-compute-directed-tree-element-𝕎 x y e) ＝ e issec-map-inv-edge-compute-directed-tree-element-𝕎 = issec-map-inv-edge-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w isretr-map-inv-edge-compute-directed-tree-element-𝕎 : (x y : node-element-𝕎 w) (e : edge-element-𝕎 w x y) → map-inv-edge-compute-directed-tree-element-𝕎 x y ( edge-compute-directed-tree-element-𝕎 x y e) ＝ e isretr-map-inv-edge-compute-directed-tree-element-𝕎 = isretr-map-inv-edge-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w is-equiv-edge-compute-directed-tree-element-𝕎 : (x y : node-element-𝕎 w) → is-equiv (edge-compute-directed-tree-element-𝕎 x y) is-equiv-edge-compute-directed-tree-element-𝕎 = is-equiv-edge-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w equiv-edge-compute-directed-tree-element-𝕎 : (x y : node-element-𝕎 w) → edge-element-𝕎 w x y ≃ edge-combinator-Directed-Tree ( λ b → directed-tree-element-𝕎 (component-𝕎 w b)) ( node-compute-directed-tree-element-𝕎 x) ( node-compute-directed-tree-element-𝕎 y) equiv-edge-compute-directed-tree-element-𝕎 = equiv-edge-compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w compute-directed-tree-element-𝕎 : equiv-Directed-Tree ( directed-tree-element-𝕎 w) ( combinator-Directed-Tree ( λ b → directed-tree-element-𝕎 (component-𝕎 w b))) compute-directed-tree-element-𝕎 = compute-directed-tree-element-coalgebra (𝕎-Coalg A B) w shape-compute-enriched-directed-tree-element-𝕎 : shape-element-𝕎 w ~ ( ( shape-combinator-Enriched-Directed-Tree A B ( λ b → enriched-directed-tree-element-𝕎 (component-𝕎 w b))) ∘ ( node-compute-directed-tree-element-𝕎)) shape-compute-enriched-directed-tree-element-𝕎 = shape-compute-enriched-directed-tree-element-coalgebra (𝕎-Coalg A B) w enrichment-compute-enriched-directed-tree-element-𝕎 : (x : node-element-𝕎 w) → htpy-equiv ( ( equiv-direct-predecessor-equiv-Directed-Tree ( directed-tree-element-𝕎 w) ( combinator-Directed-Tree ( λ b → directed-tree-element-𝕎 (component-𝕎 w b))) ( compute-directed-tree-element-𝕎) ( x)) ∘e ( enrichment-element-𝕎 w x)) ( ( enrichment-combinator-Enriched-Directed-Tree A B ( λ b → enriched-directed-tree-element-𝕎 (component-𝕎 w b)) ( node-compute-directed-tree-element-𝕎 x)) ∘e ( equiv-tr B ( shape-compute-enriched-directed-tree-element-𝕎 x))) enrichment-compute-enriched-directed-tree-element-𝕎 = enrichment-compute-enriched-directed-tree-element-coalgebra (𝕎-Coalg A B) w compute-enriched-directed-tree-element-𝕎 : equiv-Enriched-Directed-Tree A B ( enriched-directed-tree-element-𝕎 w) ( combinator-Enriched-Directed-Tree A B ( λ b → enriched-directed-tree-element-𝕎 (component-𝕎 w b))) compute-enriched-directed-tree-element-𝕎 = compute-enriched-directed-tree-element-coalgebra (𝕎-Coalg A B) w