# The underlying trees of elements of W-types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-04-10.

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.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.isolated-elements
open import foundation.negated-equality
open import foundation.propositions
open import foundation.torsorial-type-families
open import foundation.transport-along-identifications
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)

is-section-map-inv-enrichment-element-𝕎 :
(w : 𝕎 A B) (x : node-element-𝕎 w) →
( map-enrichment-element-𝕎 w x ∘
map-inv-enrichment-element-𝕎 w x) ~ id
is-section-map-inv-enrichment-element-𝕎 =
is-section-map-inv-enrichment-directed-tree-element-coalgebra (𝕎-Coalg A B)

is-retraction-map-inv-enrichment-element-𝕎 :
(w : 𝕎 A B) (x : node-element-𝕎 w) →
( map-inv-enrichment-element-𝕎 w x ∘
map-enrichment-element-𝕎 w x) ~ id
is-retraction-map-inv-enrichment-element-𝕎 =
is-retraction-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-torsorial-Eq-node-element-𝕎 :
(w : 𝕎 A B) (x : node-element-𝕎 w) →
is-torsorial (Eq-node-element-𝕎 w x)
is-torsorial-Eq-node-element-𝕎 =
is-torsorial-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

is-section-map-inv-node-compute-directed-tree-element-𝕎 :
( node-compute-directed-tree-element-𝕎 ∘
map-inv-node-compute-directed-tree-element-𝕎) ~ id
is-section-map-inv-node-compute-directed-tree-element-𝕎 =
is-section-map-inv-node-compute-directed-tree-element-coalgebra
( 𝕎-Coalg A B)
( w)

is-retraction-map-inv-node-compute-directed-tree-element-𝕎 :
( map-inv-node-compute-directed-tree-element-𝕎 ∘
node-compute-directed-tree-element-𝕎) ~ id
is-retraction-map-inv-node-compute-directed-tree-element-𝕎 =
is-retraction-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

is-section-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
is-section-map-inv-edge-compute-directed-tree-element-𝕎 =
is-section-map-inv-edge-compute-directed-tree-element-coalgebra
( 𝕎-Coalg A B)
( w)

is-retraction-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
is-retraction-map-inv-edge-compute-directed-tree-element-𝕎 =
is-retraction-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