# Raising universe levels of directed trees

Content created by Egbert Rijke.

Created on 2023-05-03.

module trees.raising-universe-levels-directed-trees where

Imports
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.raising-universe-levels
open import foundation.universe-levels

open import graph-theory.directed-graphs
open import graph-theory.raising-universe-levels-directed-graphs
open import graph-theory.walks-directed-graphs

open import trees.directed-trees
open import trees.equivalences-directed-trees


## Idea

We define the operation that raises the universe level of a directed tree.

## Definitions

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

graph-raise-Directed-Tree : Directed-Graph (l1 ⊔ l3) (l2 ⊔ l4)
graph-raise-Directed-Tree = raise-Directed-Graph l3 l4 (graph-Directed-Tree T)

node-raise-Directed-Tree : UU (l1 ⊔ l3)
node-raise-Directed-Tree = vertex-Directed-Graph graph-raise-Directed-Tree

equiv-node-compute-raise-Directed-Tree :
node-Directed-Tree T ≃ node-raise-Directed-Tree
equiv-node-compute-raise-Directed-Tree =
equiv-vertex-compute-raise-Directed-Graph l3 l4 (graph-Directed-Tree T)

node-compute-raise-Directed-Tree :
node-Directed-Tree T → node-raise-Directed-Tree
node-compute-raise-Directed-Tree =
vertex-compute-raise-Directed-Graph l3 l4 (graph-Directed-Tree T)

edge-raise-Directed-Tree :
(x y : node-raise-Directed-Tree) → UU (l2 ⊔ l4)
edge-raise-Directed-Tree = edge-Directed-Graph graph-raise-Directed-Tree

equiv-edge-compute-raise-Directed-Tree :
(x y : node-Directed-Tree T) →
edge-Directed-Tree T x y ≃
edge-raise-Directed-Tree
( node-compute-raise-Directed-Tree x)
( node-compute-raise-Directed-Tree y)
equiv-edge-compute-raise-Directed-Tree =
equiv-edge-compute-raise-Directed-Graph l3 l4 (graph-Directed-Tree T)

edge-compute-raise-Directed-Tree :
(x y : node-Directed-Tree T) →
edge-Directed-Tree T x y →
edge-raise-Directed-Tree
( node-compute-raise-Directed-Tree x)
( node-compute-raise-Directed-Tree y)
edge-compute-raise-Directed-Tree =
edge-compute-raise-Directed-Graph l3 l4 (graph-Directed-Tree T)

walk-raise-Directed-Tree :
(x y : node-raise-Directed-Tree) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
walk-raise-Directed-Tree = walk-Directed-Graph graph-raise-Directed-Tree

equiv-walk-compute-raise-Directed-Tree :
{x y : node-Directed-Tree T} →
walk-Directed-Tree T x y ≃
walk-raise-Directed-Tree
( node-compute-raise-Directed-Tree x)
( node-compute-raise-Directed-Tree y)
equiv-walk-compute-raise-Directed-Tree =
equiv-walk-compute-raise-Directed-Graph l3 l4 (graph-Directed-Tree T)

walk-compute-raise-Directed-Tree :
{x y : node-Directed-Tree T} →
walk-Directed-Tree T x y →
walk-raise-Directed-Tree
( node-compute-raise-Directed-Tree x)
( node-compute-raise-Directed-Tree y)
walk-compute-raise-Directed-Tree =
walk-compute-raise-Directed-Graph l3 l4 (graph-Directed-Tree T)

root-raise-Directed-Tree : node-raise-Directed-Tree
root-raise-Directed-Tree =
node-compute-raise-Directed-Tree (root-Directed-Tree T)

unique-walk-to-root-raise-Directed-Tree :
(x : node-raise-Directed-Tree) →
is-contr (walk-raise-Directed-Tree x root-raise-Directed-Tree)
unique-walk-to-root-raise-Directed-Tree (map-raise x) =
is-contr-equiv'
( walk-Directed-Tree T x (root-Directed-Tree T))
( equiv-walk-compute-raise-Directed-Tree)
( unique-walk-to-root-Directed-Tree T x)

is-tree-raise-Directed-Tree :
is-tree-Directed-Graph graph-raise-Directed-Tree
pr1 is-tree-raise-Directed-Tree = root-raise-Directed-Tree
pr2 is-tree-raise-Directed-Tree = unique-walk-to-root-raise-Directed-Tree

raise-Directed-Tree : Directed-Tree (l1 ⊔ l3) (l2 ⊔ l4)
pr1 raise-Directed-Tree = graph-raise-Directed-Tree
pr2 raise-Directed-Tree = is-tree-raise-Directed-Tree

compute-raise-Directed-Tree :
equiv-Directed-Tree T raise-Directed-Tree
compute-raise-Directed-Tree =
compute-raise-Directed-Graph l3 l4 (graph-Directed-Tree T)