# Bases of directed trees

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-05-03.

module trees.bases-directed-trees where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositions
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.type-arithmetic-empty-type
open import foundation.universe-levels

open import graph-theory.walks-directed-graphs

open import trees.directed-trees


## Idea

The base of a directed tree consists of the nodes equipped with an edge to the root.

## Definition

module _
{l1 l2 : Level} (T : Directed-Tree l1 l2)
where

base-Directed-Tree : UU (l1 ⊔ l2)
base-Directed-Tree = direct-predecessor-Directed-Tree T (root-Directed-Tree T)

module _
(b : base-Directed-Tree)
where

node-base-Directed-Tree : node-Directed-Tree T
node-base-Directed-Tree = pr1 b

edge-base-Directed-Tree :
edge-Directed-Tree T node-base-Directed-Tree (root-Directed-Tree T)
edge-base-Directed-Tree = pr2 b


## Properties

### The root is not a base element

module _
{l1 l2 : Level} (T : Directed-Tree l1 l2)
where

is-proper-node-base-Directed-Tree :
(b : base-Directed-Tree T) →
is-proper-node-Directed-Tree T (node-base-Directed-Tree T b)
is-proper-node-base-Directed-Tree (x , e) refl =
no-direct-successor-root-Directed-Tree T (x , e)

no-walk-to-base-root-Directed-Tree :
(b : base-Directed-Tree T) →
¬ ( walk-Directed-Tree T
( root-Directed-Tree T)
( node-base-Directed-Tree T b))
no-walk-to-base-root-Directed-Tree
( pair .(root-Directed-Tree T) e)
refl-walk-Directed-Graph =
no-direct-successor-root-Directed-Tree T (root-Directed-Tree T , e)
no-walk-to-base-root-Directed-Tree b (cons-walk-Directed-Graph e w) =
no-direct-successor-root-Directed-Tree T (_ , e)


### Any node which has a walk to a base element is a proper node

module _
{l1 l2 : Level} (T : Directed-Tree l1 l2)
where

is-proper-node-walk-to-base-Directed-Tree :
(x : node-Directed-Tree T) (b : base-Directed-Tree T) →
walk-Directed-Tree T x (node-base-Directed-Tree T b) →
is-proper-node-Directed-Tree T x
is-proper-node-walk-to-base-Directed-Tree ._ b refl-walk-Directed-Graph =
is-proper-node-base-Directed-Tree T b
is-proper-node-walk-to-base-Directed-Tree x b (cons-walk-Directed-Graph e w) =
is-proper-node-direct-successor-Directed-Tree T e


### There are no edges between base elements

module _
{l1 l2 : Level} (T : Directed-Tree l1 l2)
where

no-edge-base-Directed-Tree :
(a b : base-Directed-Tree T) →
¬ ( edge-Directed-Tree T
( node-base-Directed-Tree T a)
( node-base-Directed-Tree T b))
no-edge-base-Directed-Tree a b e =
ex-falso
( is-not-one-two-ℕ
( ap
( length-walk-Directed-Graph (graph-Directed-Tree T))
( eq-is-contr'
( unique-walk-to-root-Directed-Tree T
( node-base-Directed-Tree T a))
( cons-walk-Directed-Tree T e
( unit-walk-Directed-Tree T (edge-base-Directed-Tree T b)))
( unit-walk-Directed-Tree T (edge-base-Directed-Tree T a)))))


### For any node x, the coproduct of is-root x and the type of base elements b equipped with a walk from x to b is contractible

module _
{l1 l2 : Level} (T : Directed-Tree l1 l2)
where

cons-cases-center-walk-to-base-Directed-Tree :
{x y : node-Directed-Tree T} (e : edge-Directed-Tree T x y) →
(w : walk-Directed-Tree T y (root-Directed-Tree T)) →
Σ (base-Directed-Tree T) (walk-Directed-Tree T x ∘ pr1)
cons-cases-center-walk-to-base-Directed-Tree e refl-walk-Directed-Graph =
(_ , e) , refl-walk-Directed-Tree T
cons-cases-center-walk-to-base-Directed-Tree e
( cons-walk-Directed-Graph f w) =
tot
( λ u → cons-walk-Directed-Tree T e)
( cons-cases-center-walk-to-base-Directed-Tree f w)

cases-center-walk-to-base-Directed-Tree :
{x : node-Directed-Tree T}
(w : walk-Directed-Tree T x (root-Directed-Tree T)) →
is-root-Directed-Tree T x +
Σ (base-Directed-Tree T) (walk-Directed-Tree T x ∘ pr1)
cases-center-walk-to-base-Directed-Tree refl-walk-Directed-Graph = inl refl
cases-center-walk-to-base-Directed-Tree (cons-walk-Directed-Graph e w) =
inr (cons-cases-center-walk-to-base-Directed-Tree e w)

center-walk-to-base-Directed-Tree :
(x : node-Directed-Tree T) →
is-root-Directed-Tree T x +
Σ (base-Directed-Tree T) (walk-Directed-Tree T x ∘ pr1)
center-walk-to-base-Directed-Tree x =
cases-center-walk-to-base-Directed-Tree (walk-to-root-Directed-Tree T x)

cons-cases-contraction-walk-to-base-Directed-Tree :
{x y : node-Directed-Tree T} (e : edge-Directed-Tree T x y) →
(w : walk-Directed-Tree T y (root-Directed-Tree T))
(u : Σ (base-Directed-Tree T) (walk-Directed-Tree T x ∘ pr1)) →
cons-cases-center-walk-to-base-Directed-Tree e w ＝ u
cons-cases-contraction-walk-to-base-Directed-Tree e
( refl-walk-Directed-Graph)
( (z , f) , refl-walk-Directed-Graph) =
ap
( λ i → ((z , i) , refl-walk-Directed-Graph))
( eq-is-contr
( is-proof-irrelevant-edge-to-root-Directed-Tree T z e))
cons-cases-contraction-walk-to-base-Directed-Tree {x} e
( refl-walk-Directed-Graph)
( (z , f) , cons-walk-Directed-Graph {_} {y} g v) =
ex-falso
( no-walk-to-base-root-Directed-Tree T
( z , f)
( tr
( λ u → walk-Directed-Tree T u z)
( ap pr1
( eq-direct-successor-Directed-Tree T
( y , g)
( root-Directed-Tree T , e)))
( v)))
cons-cases-contraction-walk-to-base-Directed-Tree e
( cons-walk-Directed-Graph {y} {z} g w)
( (u , f) , refl-walk-Directed-Graph) =
ex-falso
( no-direct-successor-root-Directed-Tree T
( tr
( λ i → Σ (node-Directed-Tree T) (edge-Directed-Tree T i))
( ap pr1
( eq-direct-successor-Directed-Tree T
( y , e)
( root-Directed-Tree T , f)))
( z , g)))
cons-cases-contraction-walk-to-base-Directed-Tree {x} {y} e
( cons-walk-Directed-Graph {y} {z} g w)
( (u , f) , cons-walk-Directed-Graph {_} {y'} e' v) =
( ap
( tot (λ u → cons-walk-Directed-Tree T e))
( cons-cases-contraction-walk-to-base-Directed-Tree g w
( (u , f) ,
( tr-walk-eq-direct-successor-Directed-Tree T
( y' , e')
( y , e) v)))) ∙
( ap
( pair (u , f))
( eq-tr-walk-eq-direct-successor-Directed-Tree T (y' , e') (y , e) v))

cases-contraction-walk-to-base-Directed-Tree :
{x : node-Directed-Tree T}
(w : walk-Directed-Tree T x (root-Directed-Tree T)) →
(u :
is-root-Directed-Tree T x +
Σ (base-Directed-Tree T) (walk-Directed-Tree T x ∘ pr1)) →
cases-center-walk-to-base-Directed-Tree w ＝ u
cases-contraction-walk-to-base-Directed-Tree
( refl-walk-Directed-Graph)
( inl p) =
ap inl (eq-is-contr (is-contr-loop-space-root-Directed-Tree T))
cases-contraction-walk-to-base-Directed-Tree refl-walk-Directed-Graph
( inr (b , w)) =
ex-falso (no-walk-to-base-root-Directed-Tree T b w)
cases-contraction-walk-to-base-Directed-Tree
( cons-walk-Directed-Graph e w)
( inl refl) =
ex-falso (no-direct-successor-root-Directed-Tree T (_ , e))
cases-contraction-walk-to-base-Directed-Tree
( cons-walk-Directed-Graph e w) (inr u) =
ap inr (cons-cases-contraction-walk-to-base-Directed-Tree e w u)

contraction-walk-to-base-Directed-Tree :
(x : node-Directed-Tree T)
( w :
is-root-Directed-Tree T x +
Σ (base-Directed-Tree T) (walk-Directed-Tree T x ∘ pr1)) →
center-walk-to-base-Directed-Tree x ＝ w
contraction-walk-to-base-Directed-Tree x =
cases-contraction-walk-to-base-Directed-Tree
( walk-to-root-Directed-Tree T x)

unique-walk-to-base-Directed-Tree :
(x : node-Directed-Tree T) →
is-contr
( is-root-Directed-Tree T x +
Σ ( base-Directed-Tree T)
( walk-Directed-Tree T x ∘ node-base-Directed-Tree T))
unique-walk-to-base-Directed-Tree x =
( center-walk-to-base-Directed-Tree x ,
contraction-walk-to-base-Directed-Tree x)

is-root-or-walk-to-base-Directed-Tree :
(x : node-Directed-Tree T) →
is-root-Directed-Tree T x +
Σ ( base-Directed-Tree T)
( walk-Directed-Tree T x ∘ node-base-Directed-Tree T)
is-root-or-walk-to-base-Directed-Tree x =
center (unique-walk-to-base-Directed-Tree x)

is-root-is-root-or-walk-to-base-root-Directed-Tree :
is-root-or-walk-to-base-Directed-Tree (root-Directed-Tree T) ＝
inl refl
is-root-is-root-or-walk-to-base-root-Directed-Tree =
eq-is-contr (unique-walk-to-base-Directed-Tree (root-Directed-Tree T))

unique-walk-to-base-is-proper-node-Directed-Tree :
(x : node-Directed-Tree T) → is-proper-node-Directed-Tree T x →
is-contr
( Σ ( base-Directed-Tree T)
( walk-Directed-Tree T x ∘ node-base-Directed-Tree T))
unique-walk-to-base-is-proper-node-Directed-Tree x f =
is-contr-equiv'
( is-root-Directed-Tree T x +
Σ ( base-Directed-Tree T)
( walk-Directed-Tree T x ∘ node-base-Directed-Tree T))
( left-unit-law-coproduct-is-empty
( is-root-Directed-Tree T x)
( Σ ( base-Directed-Tree T)
( walk-Directed-Tree T x ∘ node-base-Directed-Tree T))
( f))
( unique-walk-to-base-Directed-Tree x)

walk-to-base-is-proper-node-Directed-Tree :
(x : node-Directed-Tree T) → is-proper-node-Directed-Tree T x →
Σ ( base-Directed-Tree T)
( walk-Directed-Tree T x ∘ node-base-Directed-Tree T)
walk-to-base-is-proper-node-Directed-Tree x H =
center (unique-walk-to-base-is-proper-node-Directed-Tree x H)

unique-walk-to-base-direct-successor-Directed-Tree :
(x : node-Directed-Tree T)
(u : Σ (node-Directed-Tree T) (edge-Directed-Tree T x)) →
is-contr
( Σ ( base-Directed-Tree T)
( walk-Directed-Tree T x ∘ node-base-Directed-Tree T))
unique-walk-to-base-direct-successor-Directed-Tree x u =
unique-walk-to-base-is-proper-node-Directed-Tree x
( is-proper-node-direct-successor-Directed-Tree T (pr2 u))

is-proof-irrelevant-walk-to-base-Directed-Tree :
(x : node-Directed-Tree T) →
is-proof-irrelevant
( Σ ( base-Directed-Tree T)
( λ b → walk-Directed-Tree T x (node-base-Directed-Tree T b)))
is-proof-irrelevant-walk-to-base-Directed-Tree x (b , w) =
unique-walk-to-base-is-proper-node-Directed-Tree x
( is-proper-node-walk-to-base-Directed-Tree T x b w)

is-prop-walk-to-base-Directed-Tree :
(x : node-Directed-Tree T) →
is-prop
( Σ ( base-Directed-Tree T)
( λ b → walk-Directed-Tree T x (node-base-Directed-Tree T b)))
is-prop-walk-to-base-Directed-Tree x =
is-prop-is-proof-irrelevant
( is-proof-irrelevant-walk-to-base-Directed-Tree x)

walk-to-base-Directed-Tree-Prop : node-Directed-Tree T → Prop (l1 ⊔ l2)
pr1 (walk-to-base-Directed-Tree-Prop x) =
Σ ( base-Directed-Tree T)
( λ b → walk-Directed-Tree T x (node-base-Directed-Tree T b))
pr2 (walk-to-base-Directed-Tree-Prop x) =
is-prop-walk-to-base-Directed-Tree x


### The type of proper nodes of a directed tree is equivalent to the type of nodes equipped with a base element b and a walk to b

module _
{l1 l2 : Level} (T : Directed-Tree l1 l2)
where

compute-proper-node-Directed-Tree :
proper-node-Directed-Tree T ≃
Σ ( base-Directed-Tree T)
( λ b →
Σ ( node-Directed-Tree T)
( λ x → walk-Directed-Tree T x (node-base-Directed-Tree T b)))
compute-proper-node-Directed-Tree =
( equiv-left-swap-Σ) ∘e
( equiv-tot
( λ x →
equiv-iff
( is-proper-node-Directed-Tree-Prop T x)
( walk-to-base-Directed-Tree-Prop T x)
( walk-to-base-is-proper-node-Directed-Tree T x)
( λ (b , w) → is-proper-node-walk-to-base-Directed-Tree T x b w)))

map-compute-proper-node-Directed-Tree :
proper-node-Directed-Tree T →
Σ ( base-Directed-Tree T)
( λ b →
Σ ( node-Directed-Tree T)
( λ x → walk-Directed-Tree T x (node-base-Directed-Tree T b)))
map-compute-proper-node-Directed-Tree =
map-equiv compute-proper-node-Directed-Tree

eq-compute-proper-node-Directed-Tree :
{x : node-Directed-Tree T} (H : is-proper-node-Directed-Tree T x)
(b : base-Directed-Tree T)
(w : walk-Directed-Tree T x (node-base-Directed-Tree T b)) →
map-compute-proper-node-Directed-Tree (x , H) ＝ (b , x , w)
eq-compute-proper-node-Directed-Tree {x} H b w =
ap
( map-equiv equiv-left-swap-Σ)
( eq-pair-eq-fiber (eq-is-prop (is-prop-walk-to-base-Directed-Tree T x)))