From 603f4ac4a9784dfe4de2b1bcb86532f14e96c90d Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 4 May 2023 08:47:01 +0200
Subject: [PATCH] Trees (#587)

Refactoring trees:

- renamed children to direct predecessors
- renamed parents to direct successors
- used the definition of fibers of directed graphs in the definition of
fibers of directed trees.
---
 .../fibers-directed-graphs.lagda.md           |  31 +--
 .../walks-directed-graphs.lagda.md            |   5 +-
 src/trees/bases-directed-trees.lagda.md       |  35 ++-
 .../bases-enriched-directed-trees.lagda.md    |  14 +-
 src/trees/combinator-directed-trees.lagda.md  | 148 ++++++-----
 ...ombinator-enriched-directed-trees.lagda.md |  68 ++---
 src/trees/directed-trees.lagda.md             | 239 +++++++++--------
 src/trees/enriched-directed-trees.lagda.md    |  84 +++---
 .../equivalences-directed-trees.lagda.md      |  16 +-
 ...ivalences-enriched-directed-trees.lagda.md |  44 ++--
 src/trees/fibers-directed-trees.lagda.md      | 247 ++++++++----------
 .../fibers-enriched-directed-trees.lagda.md   |  63 ++---
 src/trees/morphisms-directed-trees.lagda.md   |  16 +-
 ...morphisms-enriched-directed-trees.lagda.md |  12 +-
 .../rooted-morphisms-directed-trees.lagda.md  |  20 +-
 ...morphisms-enriched-directed-trees.lagda.md |   8 +-
 ...oalgebras-polynomial-endofunctors.lagda.md |   4 +-
 ...ying-trees-of-elements-of-w-types.lagda.md |   2 +-
 18 files changed, 545 insertions(+), 511 deletions(-)

diff --git a/src/graph-theory/fibers-directed-graphs.lagda.md b/src/graph-theory/fibers-directed-graphs.lagda.md
index 5a353909d8..28ee886810 100644
--- a/src/graph-theory/fibers-directed-graphs.lagda.md
+++ b/src/graph-theory/fibers-directed-graphs.lagda.md
@@ -124,42 +124,43 @@ module _
 ### The fiber of `G` at `x` as a directed tree
 
 ```agda
-  center-unique-parent-fiber-Directed-Graph :
+  center-unique-direct-successor-fiber-Directed-Graph :
     (y : node-fiber-Directed-Graph) →
     ( is-root-fiber-Directed-Graph y) +
     ( Σ ( node-fiber-Directed-Graph) ( edge-fiber-Directed-Graph y))
-  center-unique-parent-fiber-Directed-Graph (y , refl-walk-Directed-Graph) =
+  center-unique-direct-successor-fiber-Directed-Graph
+    ( y , refl-walk-Directed-Graph) =
     inl refl
-  center-unique-parent-fiber-Directed-Graph
+  center-unique-direct-successor-fiber-Directed-Graph
     ( y , cons-walk-Directed-Graph {y} {z} e w) = inr ((z , w) , (e , refl))
 
-  contraction-unique-parent-fiber-Directed-Graph :
+  contraction-unique-direct-successor-fiber-Directed-Graph :
     (y : node-fiber-Directed-Graph) →
     ( p :
       ( is-root-fiber-Directed-Graph y) +
       ( Σ ( node-fiber-Directed-Graph) (edge-fiber-Directed-Graph y))) →
-    center-unique-parent-fiber-Directed-Graph y ＝ p
-  contraction-unique-parent-fiber-Directed-Graph ._ (inl refl) = refl
-  contraction-unique-parent-fiber-Directed-Graph
+    center-unique-direct-successor-fiber-Directed-Graph y ＝ p
+  contraction-unique-direct-successor-fiber-Directed-Graph ._ (inl refl) = refl
+  contraction-unique-direct-successor-fiber-Directed-Graph
     ( y , .(cons-walk-Directed-Graph e v)) (inr ((z , v) , e , refl)) =
     refl
 
-  unique-parent-fiber-Directed-Graph :
-    unique-parent-Directed-Graph
+  unique-direct-successor-fiber-Directed-Graph :
+    unique-direct-successor-Directed-Graph
       ( graph-fiber-Directed-Graph)
       ( root-fiber-Directed-Graph)
-  pr1 (unique-parent-fiber-Directed-Graph y) =
-    center-unique-parent-fiber-Directed-Graph y
-  pr2 (unique-parent-fiber-Directed-Graph y) =
-    contraction-unique-parent-fiber-Directed-Graph y
+  pr1 (unique-direct-successor-fiber-Directed-Graph y) =
+    center-unique-direct-successor-fiber-Directed-Graph y
+  pr2 (unique-direct-successor-fiber-Directed-Graph y) =
+    contraction-unique-direct-successor-fiber-Directed-Graph y
 
   is-tree-fiber-Directed-Graph :
     is-tree-Directed-Graph graph-fiber-Directed-Graph
   is-tree-fiber-Directed-Graph =
-    is-tree-unique-parent-Directed-Graph
+    is-tree-unique-direct-successor-Directed-Graph
       graph-fiber-Directed-Graph
       root-fiber-Directed-Graph
-      unique-parent-fiber-Directed-Graph
+      unique-direct-successor-fiber-Directed-Graph
       walk-to-root-fiber-Directed-Graph
 
   fiber-Directed-Graph : Directed-Tree (l1 ⊔ l2) (l1 ⊔ l2)
diff --git a/src/graph-theory/walks-directed-graphs.lagda.md b/src/graph-theory/walks-directed-graphs.lagda.md
index a6dfb7ba6c..835ff7dffd 100644
--- a/src/graph-theory/walks-directed-graphs.lagda.md
+++ b/src/graph-theory/walks-directed-graphs.lagda.md
@@ -422,13 +422,14 @@ module _
   {l1 l2 : Level} (G : Directed-Graph l1 l2) (x : vertex-Directed-Graph G)
   where
 
-  eq-parent-eq-cons-walk-Directed-Graph :
+  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-parent-eq-cons-walk-Directed-Graph {y} {.y} {z} e .e w .w refl = refl
+  eq-direct-successor-eq-cons-walk-Directed-Graph {y} {.y} {z} e .e w .w refl =
+    refl
 ```
 
 ### Vertices on a walk
diff --git a/src/trees/bases-directed-trees.lagda.md b/src/trees/bases-directed-trees.lagda.md
index 3b1735a3ad..e21a341ac4 100644
--- a/src/trees/bases-directed-trees.lagda.md
+++ b/src/trees/bases-directed-trees.lagda.md
@@ -44,7 +44,7 @@ module _
   where
 
   base-Directed-Tree : UU (l1 ⊔ l2)
-  base-Directed-Tree = children-Directed-Tree T (root-Directed-Tree T)
+  base-Directed-Tree = direct-predecessor-Directed-Tree T (root-Directed-Tree T)
 
   module _
     (b : base-Directed-Tree)
@@ -71,7 +71,7 @@ module _
     (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-parent-root-Directed-Tree T (x , e)
+    no-direct-successor-root-Directed-Tree T (x , e)
 
   no-walk-to-base-root-Directed-Tree :
     (b : base-Directed-Tree T) →
@@ -81,9 +81,9 @@ module _
   no-walk-to-base-root-Directed-Tree
     ( pair .(root-Directed-Tree T) e)
     refl-walk-Directed-Graph =
-    no-parent-root-Directed-Tree T (root-Directed-Tree T , e)
+    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-parent-root-Directed-Tree T (_ , e)
+    no-direct-successor-root-Directed-Tree T (_ , e)
 ```
 
 ### Any node which has a walk to a base element is a proper node
@@ -100,7 +100,7 @@ module _
   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-parent-Directed-Tree T e
+    is-proper-node-direct-successor-Directed-Tree T e
 ```
 
 ### There are no edges between base elements
@@ -184,17 +184,21 @@ module _
         ( tr
           ( λ u → walk-Directed-Tree T u z)
           ( ap pr1
-            ( eq-parent-Directed-Tree T (y , g) (root-Directed-Tree T , e)))
+            ( 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-parent-root-Directed-Tree T
+      ( no-direct-successor-root-Directed-Tree T
         ( tr
           ( λ i → Σ (node-Directed-Tree T) (edge-Directed-Tree T i))
           ( ap pr1
-            ( eq-parent-Directed-Tree T (y , e) (root-Directed-Tree T , f)))
+            ( 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)
@@ -202,10 +206,13 @@ module _
     ( ap
       ( tot (λ u → cons-walk-Directed-Tree T e))
       ( cons-cases-contraction-walk-to-base-Directed-Tree g w
-        ( (u , f) , tr-walk-eq-parent-Directed-Tree T (y' , e') (y , e) v))) ∙
+        ( (u , f) ,
+          ( tr-walk-eq-direct-successor-Directed-Tree T
+            ( y' , e')
+            ( y , e) v)))) ∙
     ( ap
       ( pair (u , f))
-      ( eq-tr-walk-eq-parent-Directed-Tree T (y' , e') (y , e) v))
+      ( 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}
@@ -224,7 +231,7 @@ module _
   cases-contraction-walk-to-base-Directed-Tree
     ( cons-walk-Directed-Graph e w)
     ( inl refl) =
-    ex-falso (no-parent-root-Directed-Tree T (_ , e))
+    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)
@@ -287,15 +294,15 @@ module _
   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-parent-Directed-Tree :
+  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-parent-Directed-Tree x u =
+  unique-walk-to-base-direct-successor-Directed-Tree x u =
     unique-walk-to-base-is-proper-node-Directed-Tree x
-      ( is-proper-node-parent-Directed-Tree T (pr2 u))
+      ( is-proper-node-direct-successor-Directed-Tree T (pr2 u))
 
   is-proof-irrelevant-walk-to-base-Directed-Tree :
     (x : node-Directed-Tree T) →
diff --git a/src/trees/bases-enriched-directed-trees.lagda.md b/src/trees/bases-enriched-directed-trees.lagda.md
index 5bae4d1b81..2f885e1988 100644
--- a/src/trees/bases-enriched-directed-trees.lagda.md
+++ b/src/trees/bases-enriched-directed-trees.lagda.md
@@ -43,13 +43,15 @@ module _
 
   compute-base-Enriched-Directed-Tree :
     base-Enriched-Directed-Tree ≃
-    children-Enriched-Directed-Tree A B T (root-Enriched-Directed-Tree A B T)
+    direct-predecessor-Enriched-Directed-Tree A B T
+      ( root-Enriched-Directed-Tree A B T)
   compute-base-Enriched-Directed-Tree =
     enrichment-Enriched-Directed-Tree A B T (root-Enriched-Directed-Tree A B T)
 
   map-compute-base-Enriched-Directed-Tree :
     base-Enriched-Directed-Tree →
-    children-Enriched-Directed-Tree A B T (root-Enriched-Directed-Tree A B T)
+    direct-predecessor-Enriched-Directed-Tree A B T
+      ( root-Enriched-Directed-Tree A B T)
   map-compute-base-Enriched-Directed-Tree =
     map-enrichment-Enriched-Directed-Tree A B T
       ( root-Enriched-Directed-Tree A B T)
@@ -142,7 +144,7 @@ module _
   unique-walk-to-base-Enriched-Directed-Tree x =
     is-contr-equiv
       ( is-root-Enriched-Directed-Tree A B T x +
-        Σ ( children-Enriched-Directed-Tree A B T
+        Σ ( direct-predecessor-Enriched-Directed-Tree A B T
             ( root-Enriched-Directed-Tree A B T))
           ( walk-Enriched-Directed-Tree A B T x ∘ pr1))
       ( equiv-coprod
@@ -194,7 +196,7 @@ module _
         ( f))
       ( unique-walk-to-base-Enriched-Directed-Tree x)
 
-  unique-walk-to-base-parent-Enriched-Directed-Tree :
+  unique-walk-to-base-direct-successor-Enriched-Directed-Tree :
     (x : node-Enriched-Directed-Tree A B T)
     (u :
       Σ ( node-Enriched-Directed-Tree A B T)
@@ -203,7 +205,7 @@ module _
       ( Σ ( base-Enriched-Directed-Tree A B T)
           ( walk-Enriched-Directed-Tree A B T x ∘
             node-base-Enriched-Directed-Tree A B T))
-  unique-walk-to-base-parent-Enriched-Directed-Tree x (y , e) =
+  unique-walk-to-base-direct-successor-Enriched-Directed-Tree x (y , e) =
     unique-walk-to-base-is-not-root-Enriched-Directed-Tree x
-      ( is-proper-node-parent-Enriched-Directed-Tree A B T e)
+      ( is-proper-node-direct-successor-Enriched-Directed-Tree A B T e)
 ```
diff --git a/src/trees/combinator-directed-trees.lagda.md b/src/trees/combinator-directed-trees.lagda.md
index 1115ba01e8..c7384be68b 100644
--- a/src/trees/combinator-directed-trees.lagda.md
+++ b/src/trees/combinator-directed-trees.lagda.md
@@ -129,88 +129,91 @@ module _
     ( node-inclusion-combinator-Directed-Tree i x) =
     inr (λ ())
 
-  cases-center-unique-parent-combinator-Directed-Tree' :
+  cases-center-unique-direct-successor-combinator-Directed-Tree' :
     (i : I) (x : node-Directed-Tree (T i)) →
     is-decidable (is-root-Directed-Tree (T i) x) →
     Σ ( node-combinator-Directed-Tree)
       ( edge-combinator-Directed-Tree
         ( node-inclusion-combinator-Directed-Tree i x))
-  cases-center-unique-parent-combinator-Directed-Tree' a ._ (inl refl) =
+  cases-center-unique-direct-successor-combinator-Directed-Tree' a ._
+    ( inl refl) =
     ( root-combinator-Directed-Tree , edge-to-root-combinator-Directed-Tree a)
-  cases-center-unique-parent-combinator-Directed-Tree' i x (inr f) =
+  cases-center-unique-direct-successor-combinator-Directed-Tree' i x (inr f) =
     map-Σ
       ( edge-combinator-Directed-Tree
         ( node-inclusion-combinator-Directed-Tree i x))
       ( node-inclusion-combinator-Directed-Tree i)
       ( edge-inclusion-combinator-Directed-Tree i x)
-      ( parent-is-proper-node-Directed-Tree (T i) x f)
+      ( direct-successor-is-proper-node-Directed-Tree (T i) x f)
 
-  center-unique-parent-combinator-Directed-Tree' :
+  center-unique-direct-successor-combinator-Directed-Tree' :
     ( x : node-combinator-Directed-Tree) →
     ¬ (is-root-combinator-Directed-Tree x) →
     Σ node-combinator-Directed-Tree (edge-combinator-Directed-Tree x)
-  center-unique-parent-combinator-Directed-Tree'
+  center-unique-direct-successor-combinator-Directed-Tree'
     root-combinator-Directed-Tree f = ex-falso (f refl)
-  center-unique-parent-combinator-Directed-Tree'
+  center-unique-direct-successor-combinator-Directed-Tree'
     ( node-inclusion-combinator-Directed-Tree i x) f =
-    cases-center-unique-parent-combinator-Directed-Tree' i x
+    cases-center-unique-direct-successor-combinator-Directed-Tree' i x
       ( is-isolated-root-Directed-Tree (T i) x)
 
-  cases-center-unique-parent-combinator-Directed-Tree :
+  cases-center-unique-direct-successor-combinator-Directed-Tree :
     (i : I) (x : node-Directed-Tree (T i)) →
     is-decidable (is-root-Directed-Tree (T i) x) →
     Σ ( node-combinator-Directed-Tree)
       ( edge-combinator-Directed-Tree
         ( node-inclusion-combinator-Directed-Tree i x))
-  cases-center-unique-parent-combinator-Directed-Tree i ._ (inl refl) =
+  cases-center-unique-direct-successor-combinator-Directed-Tree i ._
+    ( inl refl) =
     root-combinator-Directed-Tree ,
     edge-to-root-combinator-Directed-Tree i
-  cases-center-unique-parent-combinator-Directed-Tree i x (inr f) =
+  cases-center-unique-direct-successor-combinator-Directed-Tree i x (inr f) =
     map-Σ
       ( edge-combinator-Directed-Tree
         ( node-inclusion-combinator-Directed-Tree i x))
       ( node-inclusion-combinator-Directed-Tree i)
       ( edge-inclusion-combinator-Directed-Tree i x)
-      ( parent-is-proper-node-Directed-Tree (T i) x f)
+      ( direct-successor-is-proper-node-Directed-Tree (T i) x f)
 
-  center-unique-parent-combinator-Directed-Tree :
+  center-unique-direct-successor-combinator-Directed-Tree :
     (x : node-combinator-Directed-Tree) →
     is-root-combinator-Directed-Tree x +
     Σ node-combinator-Directed-Tree (edge-combinator-Directed-Tree x)
-  center-unique-parent-combinator-Directed-Tree root-combinator-Directed-Tree =
+  center-unique-direct-successor-combinator-Directed-Tree
+    root-combinator-Directed-Tree =
     inl refl
-  center-unique-parent-combinator-Directed-Tree
+  center-unique-direct-successor-combinator-Directed-Tree
     ( node-inclusion-combinator-Directed-Tree i x) =
     inr
-      ( cases-center-unique-parent-combinator-Directed-Tree i x
+      ( cases-center-unique-direct-successor-combinator-Directed-Tree i x
         ( is-isolated-root-Directed-Tree (T i) x))
 
-  cases-contraction-unique-parent-combinator-Directed-Tree :
+  cases-contraction-unique-direct-successor-combinator-Directed-Tree :
     (i : I) (x : node-Directed-Tree (T i)) →
     (d : is-decidable (is-root-Directed-Tree (T i) x)) →
     ( p :
       Σ ( node-combinator-Directed-Tree)
         ( edge-combinator-Directed-Tree
           ( node-inclusion-combinator-Directed-Tree i x))) →
-    cases-center-unique-parent-combinator-Directed-Tree i x d ＝ p
-  cases-contraction-unique-parent-combinator-Directed-Tree i ._
+    cases-center-unique-direct-successor-combinator-Directed-Tree i x d ＝ p
+  cases-contraction-unique-direct-successor-combinator-Directed-Tree i ._
     ( inl r)
     ( ._ , edge-to-root-combinator-Directed-Tree .i) =
     ap
       ( λ u →
-        cases-center-unique-parent-combinator-Directed-Tree i
+        cases-center-unique-direct-successor-combinator-Directed-Tree i
           ( root-Directed-Tree (T i))
           ( inl u))
       ( eq-refl-root-Directed-Tree (T i) r)
-  cases-contraction-unique-parent-combinator-Directed-Tree i ._
+  cases-contraction-unique-direct-successor-combinator-Directed-Tree i ._
     ( inr f)
     ( ._ , edge-to-root-combinator-Directed-Tree .i) =
     ex-falso (f refl)
-  cases-contraction-unique-parent-combinator-Directed-Tree i ._
+  cases-contraction-unique-direct-successor-combinator-Directed-Tree i ._
     ( inl refl)
     ( ._ , edge-inclusion-combinator-Directed-Tree .i ._ y e) =
-    ex-falso (no-parent-root-Directed-Tree (T i) (y , e))
-  cases-contraction-unique-parent-combinator-Directed-Tree i x
+    ex-falso (no-direct-successor-root-Directed-Tree (T i) (y , e))
+  cases-contraction-unique-direct-successor-combinator-Directed-Tree i x
     ( inr f)
     ( ._ , edge-inclusion-combinator-Directed-Tree .i .x y e) =
     ap
@@ -219,39 +222,41 @@ module _
           ( node-inclusion-combinator-Directed-Tree i x))
         ( node-inclusion-combinator-Directed-Tree i)
         ( edge-inclusion-combinator-Directed-Tree i x))
-      ( eq-is-contr (unique-parent-is-proper-node-Directed-Tree (T i) x f))
+      ( eq-is-contr
+        ( unique-direct-successor-is-proper-node-Directed-Tree (T i) x f))
 
-  contraction-unique-parent-combinator-Directed-Tree :
+  contraction-unique-direct-successor-combinator-Directed-Tree :
     (x : node-combinator-Directed-Tree) →
     (p : is-root-combinator-Directed-Tree x +
          Σ node-combinator-Directed-Tree (edge-combinator-Directed-Tree x)) →
-    center-unique-parent-combinator-Directed-Tree x ＝ p
-  contraction-unique-parent-combinator-Directed-Tree ._ (inl refl) = refl
-  contraction-unique-parent-combinator-Directed-Tree
+    center-unique-direct-successor-combinator-Directed-Tree x ＝ p
+  contraction-unique-direct-successor-combinator-Directed-Tree ._ (inl refl) =
+    refl
+  contraction-unique-direct-successor-combinator-Directed-Tree
     ( node-inclusion-combinator-Directed-Tree i x)
     ( inr (y , e)) =
     ap
       ( inr)
-      ( cases-contraction-unique-parent-combinator-Directed-Tree i x
+      ( cases-contraction-unique-direct-successor-combinator-Directed-Tree i x
         ( is-isolated-root-Directed-Tree (T i) x)
         ( y , e))
 
-  unique-parent-combinator-Directed-Tree :
-    unique-parent-Directed-Graph
+  unique-direct-successor-combinator-Directed-Tree :
+    unique-direct-successor-Directed-Graph
       ( graph-combinator-Directed-Tree)
       ( root-combinator-Directed-Tree)
-  pr1 (unique-parent-combinator-Directed-Tree x) =
-    center-unique-parent-combinator-Directed-Tree x
-  pr2 (unique-parent-combinator-Directed-Tree x) =
-    contraction-unique-parent-combinator-Directed-Tree x
+  pr1 (unique-direct-successor-combinator-Directed-Tree x) =
+    center-unique-direct-successor-combinator-Directed-Tree x
+  pr2 (unique-direct-successor-combinator-Directed-Tree x) =
+    contraction-unique-direct-successor-combinator-Directed-Tree x
 
   is-tree-combinator-Directed-Tree :
     is-tree-Directed-Graph graph-combinator-Directed-Tree
   is-tree-combinator-Directed-Tree =
-    is-tree-unique-parent-Directed-Graph
+    is-tree-unique-direct-successor-Directed-Graph
       graph-combinator-Directed-Tree
       root-combinator-Directed-Tree
-      unique-parent-combinator-Directed-Tree
+      unique-direct-successor-combinator-Directed-Tree
       walk-to-root-combinator-Directed-Tree
 
   combinator-Directed-Tree : Directed-Tree (l1 ⊔ l2) (l1 ⊔ l2 ⊔ l3)
@@ -279,7 +284,7 @@ module _
 
 ## Properties
 
-### The type of children of `x : T i` is equivalent to the type of children of the inclusion of `x` in `combinator T`
+### The type of direct predecessors of `x : T i` is equivalent to the type of direct predecessors of the inclusion of `x` in `combinator T`
 
 ```agda
 module _
@@ -287,53 +292,56 @@ module _
   (i : I) (x : node-Directed-Tree (T i))
   where
 
-  children-combinator-Directed-Tree : UU (l1 ⊔ l2 ⊔ l3)
-  children-combinator-Directed-Tree =
+  direct-predecessor-combinator-Directed-Tree : UU (l1 ⊔ l2 ⊔ l3)
+  direct-predecessor-combinator-Directed-Tree =
     Σ ( node-combinator-Directed-Tree T)
       ( λ y →
         edge-combinator-Directed-Tree T y
           ( node-inclusion-combinator-Directed-Tree i x))
 
-  map-compute-children-combinator-Directed-Tree :
-    children-Directed-Tree (T i) x → children-combinator-Directed-Tree
-  pr1 (map-compute-children-combinator-Directed-Tree (y , e)) =
+  map-compute-direct-predecessor-combinator-Directed-Tree :
+    direct-predecessor-Directed-Tree (T i) x →
+    direct-predecessor-combinator-Directed-Tree
+  pr1 (map-compute-direct-predecessor-combinator-Directed-Tree (y , e)) =
     node-inclusion-combinator-Directed-Tree i y
-  pr2 (map-compute-children-combinator-Directed-Tree (y , e)) =
+  pr2 (map-compute-direct-predecessor-combinator-Directed-Tree (y , e)) =
     edge-inclusion-combinator-Directed-Tree i y x e
 
-  map-inv-compute-children-combinator-Directed-Tree :
-    children-combinator-Directed-Tree →
-    children-Directed-Tree (T i) x
-  map-inv-compute-children-combinator-Directed-Tree
+  map-inv-compute-direct-predecessor-combinator-Directed-Tree :
+    direct-predecessor-combinator-Directed-Tree →
+    direct-predecessor-Directed-Tree (T i) x
+  map-inv-compute-direct-predecessor-combinator-Directed-Tree
     ( ._ , edge-inclusion-combinator-Directed-Tree .i y .x e) =
     ( y , e)
 
-  issec-map-inv-compute-children-combinator-Directed-Tree :
-    ( map-compute-children-combinator-Directed-Tree ∘
-      map-inv-compute-children-combinator-Directed-Tree) ~ id
-  issec-map-inv-compute-children-combinator-Directed-Tree
+  issec-map-inv-compute-direct-predecessor-combinator-Directed-Tree :
+    ( map-compute-direct-predecessor-combinator-Directed-Tree ∘
+      map-inv-compute-direct-predecessor-combinator-Directed-Tree) ~ id
+  issec-map-inv-compute-direct-predecessor-combinator-Directed-Tree
     ( ._ , edge-inclusion-combinator-Directed-Tree .i y .x e) =
     refl
 
-  isretr-map-inv-compute-children-combinator-Directed-Tree :
-    ( map-inv-compute-children-combinator-Directed-Tree ∘
-      map-compute-children-combinator-Directed-Tree) ~ id
-  isretr-map-inv-compute-children-combinator-Directed-Tree (y , e) = refl
+  isretr-map-inv-compute-direct-predecessor-combinator-Directed-Tree :
+    ( map-inv-compute-direct-predecessor-combinator-Directed-Tree ∘
+      map-compute-direct-predecessor-combinator-Directed-Tree) ~ id
+  isretr-map-inv-compute-direct-predecessor-combinator-Directed-Tree (y , e) =
+    refl
 
-  is-equiv-map-compute-children-combinator-Directed-Tree :
-    is-equiv map-compute-children-combinator-Directed-Tree
-  is-equiv-map-compute-children-combinator-Directed-Tree =
+  is-equiv-map-compute-direct-predecessor-combinator-Directed-Tree :
+    is-equiv map-compute-direct-predecessor-combinator-Directed-Tree
+  is-equiv-map-compute-direct-predecessor-combinator-Directed-Tree =
     is-equiv-has-inverse
-      map-inv-compute-children-combinator-Directed-Tree
-      issec-map-inv-compute-children-combinator-Directed-Tree
-      isretr-map-inv-compute-children-combinator-Directed-Tree
-
-  compute-children-combinator-Directed-Tree :
-    children-Directed-Tree (T i) x ≃ children-combinator-Directed-Tree
-  pr1 compute-children-combinator-Directed-Tree =
-    map-compute-children-combinator-Directed-Tree
-  pr2 compute-children-combinator-Directed-Tree =
-    is-equiv-map-compute-children-combinator-Directed-Tree
+      map-inv-compute-direct-predecessor-combinator-Directed-Tree
+      issec-map-inv-compute-direct-predecessor-combinator-Directed-Tree
+      isretr-map-inv-compute-direct-predecessor-combinator-Directed-Tree
+
+  compute-direct-predecessor-combinator-Directed-Tree :
+    direct-predecessor-Directed-Tree (T i) x ≃
+    direct-predecessor-combinator-Directed-Tree
+  pr1 compute-direct-predecessor-combinator-Directed-Tree =
+    map-compute-direct-predecessor-combinator-Directed-Tree
+  pr2 compute-direct-predecessor-combinator-Directed-Tree =
+    is-equiv-map-compute-direct-predecessor-combinator-Directed-Tree
 ```
 
 ### If `e` is an edge from `node-inclusion i x` to `node-inclusion j y`, then `i ＝ j`
diff --git a/src/trees/combinator-enriched-directed-trees.lagda.md b/src/trees/combinator-enriched-directed-trees.lagda.md
index b8225aca58..76ff82c55f 100644
--- a/src/trees/combinator-enriched-directed-trees.lagda.md
+++ b/src/trees/combinator-enriched-directed-trees.lagda.md
@@ -115,12 +115,12 @@ module _
     is-root-combinator-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B ∘ T)
 
-  unique-parent-combinator-Enriched-Directed-Tree :
-    unique-parent-Directed-Graph
+  unique-direct-successor-combinator-Enriched-Directed-Tree :
+    unique-direct-successor-Directed-Graph
       ( graph-combinator-Enriched-Directed-Tree)
       ( root-combinator-Enriched-Directed-Tree)
-  unique-parent-combinator-Enriched-Directed-Tree =
-    unique-parent-combinator-Directed-Tree
+  unique-direct-successor-combinator-Enriched-Directed-Tree =
+    unique-direct-successor-combinator-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B ∘ T)
 
   is-tree-combinator-Enriched-Directed-Tree :
@@ -218,7 +218,7 @@ module _
     root-enrichment-combinator-Enriched-Directed-Tree
   enrichment-combinator-Enriched-Directed-Tree
     ( node-inclusion-combinator-Directed-Tree b x) =
-    ( compute-children-combinator-Directed-Tree
+    ( compute-direct-predecessor-combinator-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B ∘ T) b x) ∘e
     ( enrichment-Enriched-Directed-Tree A B (T b) x)
 
@@ -234,7 +234,7 @@ module _
 
 ## Properties
 
-### The type of children of `x : T b` is equivalent to the type of children of the inclusion of `x` in `combinator T`
+### The type of direct-predecessor of `x : T b` is equivalent to the type of direct-predecessor of the inclusion of `x` in `combinator T`
 
 ```agda
 module _
@@ -243,35 +243,35 @@ module _
   (x : node-Enriched-Directed-Tree A B (T b))
   where
 
-  children-combinator-Enriched-Directed-Tree : UU (l2 ⊔ l3 ⊔ l4)
-  children-combinator-Enriched-Directed-Tree =
-    children-combinator-Directed-Tree
+  direct-predecessor-combinator-Enriched-Directed-Tree : UU (l2 ⊔ l3 ⊔ l4)
+  direct-predecessor-combinator-Enriched-Directed-Tree =
+    direct-predecessor-combinator-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B ∘ T)
       ( b)
       ( x)
 
-  map-compute-children-combinator-Enriched-Directed-Tree :
-    children-Enriched-Directed-Tree A B (T b) x →
-    children-combinator-Enriched-Directed-Tree
-  map-compute-children-combinator-Enriched-Directed-Tree =
-    map-compute-children-combinator-Directed-Tree
+  map-compute-direct-predecessor-combinator-Enriched-Directed-Tree :
+    direct-predecessor-Enriched-Directed-Tree A B (T b) x →
+    direct-predecessor-combinator-Enriched-Directed-Tree
+  map-compute-direct-predecessor-combinator-Enriched-Directed-Tree =
+    map-compute-direct-predecessor-combinator-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B ∘ T)
       ( b)
       ( x)
 
-  is-equiv-map-compute-children-combinator-Enriched-Directed-Tree :
-    is-equiv map-compute-children-combinator-Enriched-Directed-Tree
-  is-equiv-map-compute-children-combinator-Enriched-Directed-Tree =
-    is-equiv-map-compute-children-combinator-Directed-Tree
+  is-equiv-map-compute-direct-predecessor-combinator-Enriched-Directed-Tree :
+    is-equiv map-compute-direct-predecessor-combinator-Enriched-Directed-Tree
+  is-equiv-map-compute-direct-predecessor-combinator-Enriched-Directed-Tree =
+    is-equiv-map-compute-direct-predecessor-combinator-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B ∘ T)
       ( b)
       ( x)
 
-  compute-children-combinator-Enriched-Directed-Tree :
-    children-Enriched-Directed-Tree A B (T b) x ≃
-    children-combinator-Enriched-Directed-Tree
-  compute-children-combinator-Enriched-Directed-Tree =
-    compute-children-combinator-Directed-Tree
+  compute-direct-predecessor-combinator-Enriched-Directed-Tree :
+    direct-predecessor-Enriched-Directed-Tree A B (T b) x ≃
+    direct-predecessor-combinator-Enriched-Directed-Tree
+  compute-direct-predecessor-combinator-Enriched-Directed-Tree =
+    compute-direct-predecessor-combinator-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B ∘ T)
       ( b)
       ( x)
@@ -497,15 +497,15 @@ module _
     hom-fiber-combinator-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B ∘ T)
 
-  children-compute-fiber-combinator-Enriched-Directed-Tree :
+  direct-predecessor-compute-fiber-combinator-Enriched-Directed-Tree :
     (b : B a) (x : node-Enriched-Directed-Tree A B (T b)) →
-    children-Enriched-Directed-Tree A B (T b) x →
-    children-fiber-Enriched-Directed-Tree A B
+    direct-predecessor-Enriched-Directed-Tree A B (T b) x →
+    direct-predecessor-fiber-Enriched-Directed-Tree A B
       ( combinator-Enriched-Directed-Tree A B T)
       ( node-base-index-combinator-Enriched-Directed-Tree A B T b)
       ( node-compute-fiber-combinator-Enriched-Directed-Tree b x)
-  children-compute-fiber-combinator-Enriched-Directed-Tree b =
-    children-hom-Directed-Tree
+  direct-predecessor-compute-fiber-combinator-Enriched-Directed-Tree b =
+    direct-predecessor-hom-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B (T b))
       ( directed-tree-fiber-Enriched-Directed-Tree A B
         ( combinator-Enriched-Directed-Tree A B T)
@@ -546,7 +546,9 @@ module _
 
   enrichment-compute-fiber-combinator-Enriched-Directed-Tree :
     (b : B a) (x : node-Enriched-Directed-Tree A B (T b)) →
-    ( ( children-compute-fiber-combinator-Enriched-Directed-Tree b x) ∘
+    ( ( direct-predecessor-compute-fiber-combinator-Enriched-Directed-Tree
+        ( b)
+        ( x)) ∘
       ( map-enrichment-Enriched-Directed-Tree A B (T b) x)) ~
     ( map-enrichment-fiber-base-Enriched-Directed-Tree A B
         ( combinator-Enriched-Directed-Tree A B T)
@@ -560,11 +562,15 @@ module _
       ( y)
       ( pr2
         ( pr1
-          ( children-compute-fiber-combinator-Enriched-Directed-Tree b x
+          ( direct-predecessor-compute-fiber-combinator-Enriched-Directed-Tree
+            ( b)
+            ( x)
             ( map-enrichment-Enriched-Directed-Tree A B (T b) x y))))
       ( pr2
         ( pr2
-          ( children-compute-fiber-combinator-Enriched-Directed-Tree b x
+          ( direct-predecessor-compute-fiber-combinator-Enriched-Directed-Tree
+            ( b)
+            ( x)
             ( map-enrichment-Enriched-Directed-Tree A B (T b) x y))))
 
   compute-fiber-combinator-Enriched-Directed-Tree :
diff --git a/src/trees/directed-trees.lagda.md b/src/trees/directed-trees.lagda.md
index cc5462a616..331f790d02 100644
--- a/src/trees/directed-trees.lagda.md
+++ b/src/trees/directed-trees.lagda.md
@@ -1,5 +1,7 @@
 # Directed trees
 
+!
+
 ```agda
 module trees.directed-trees where
 ```
@@ -87,17 +89,19 @@ module _
   edge-Directed-Tree : (x y : node-Directed-Tree) → UU l2
   edge-Directed-Tree = edge-Directed-Graph graph-Directed-Tree
 
-  children-Directed-Tree : node-Directed-Tree → UU (l1 ⊔ l2)
-  children-Directed-Tree x = Σ node-Directed-Tree (λ y → edge-Directed-Tree y x)
+  direct-predecessor-Directed-Tree : node-Directed-Tree → UU (l1 ⊔ l2)
+  direct-predecessor-Directed-Tree x =
+    Σ node-Directed-Tree (λ y → edge-Directed-Tree y x)
 
-  node-children-Directed-Tree :
-    (x : node-Directed-Tree) → children-Directed-Tree x → node-Directed-Tree
-  node-children-Directed-Tree x = pr1
+  node-direct-predecessor-Directed-Tree :
+    (x : node-Directed-Tree) →
+    direct-predecessor-Directed-Tree x → node-Directed-Tree
+  node-direct-predecessor-Directed-Tree x = pr1
 
-  edge-children-Directed-Tree :
-    (x : node-Directed-Tree) (y : children-Directed-Tree x) →
-    edge-Directed-Tree (node-children-Directed-Tree x y) x
-  edge-children-Directed-Tree x = pr2
+  edge-direct-predecessor-Directed-Tree :
+    (x : node-Directed-Tree) (y : direct-predecessor-Directed-Tree x) →
+    edge-Directed-Tree (node-direct-predecessor-Directed-Tree x y) x
+  edge-direct-predecessor-Directed-Tree x = pr2
 
   walk-Directed-Tree : (x y : node-Directed-Tree) → UU (l1 ⊔ l2)
   walk-Directed-Tree = walk-Directed-Graph graph-Directed-Tree
@@ -303,16 +307,16 @@ module _
     eq-is-contr is-contr-loop-space-root-Directed-Tree
 ```
 
-### The root has no parents
+### The root has no direct successors
 
 ```agda
 module _
   {l1 l2 : Level} (T : Directed-Tree l1 l2)
   where
 
-  no-parent-root-Directed-Tree :
+  no-direct-successor-root-Directed-Tree :
     ¬ (Σ (node-Directed-Tree T) (edge-Directed-Tree T (root-Directed-Tree T)))
-  no-parent-root-Directed-Tree (x , e) =
+  no-direct-successor-root-Directed-Tree (x , e) =
     neq-cons-refl-walk-Directed-Graph
       ( graph-Directed-Tree T)
       ( root-Directed-Tree T)
@@ -322,11 +326,11 @@ module _
       ( eq-is-contr
         ( unique-walk-to-root-Directed-Tree T (root-Directed-Tree T)))
 
-  is-proper-node-parent-Directed-Tree :
+  is-proper-node-direct-successor-Directed-Tree :
     {x y : node-Directed-Tree T} (e : edge-Directed-Tree T x y) →
     ¬ (is-root-Directed-Tree T x)
-  is-proper-node-parent-Directed-Tree e refl =
-    no-parent-root-Directed-Tree (_ , e)
+  is-proper-node-direct-successor-Directed-Tree e refl =
+    no-direct-successor-root-Directed-Tree (_ , e)
 ```
 
 ### The type of edges to the root is a proposition
@@ -359,88 +363,92 @@ module _
     eq-is-prop (is-prop-edge-to-root-Directed-Tree x)
 ```
 
-### Graphs in which vertices have unique parents are trees if for every vertex `x` there is a walk from `x` to the root
+### Graphs in which vertices have unique direct-successors are trees if for every vertex `x` there is a walk from `x` to the root
 
 ```agda
 module _
   {l1 l2 : Level} (G : Directed-Graph l1 l2) (r : vertex-Directed-Graph G)
   where
 
-  unique-parent-Directed-Graph : UU (l1 ⊔ l2)
-  unique-parent-Directed-Graph =
+  unique-direct-successor-Directed-Graph : UU (l1 ⊔ l2)
+  unique-direct-successor-Directed-Graph =
     (x : vertex-Directed-Graph G) →
     is-contr ((r ＝ x) + Σ (vertex-Directed-Graph G) (edge-Directed-Graph G x))
 
-  no-parent-root-unique-parent-Directed-Graph :
-    unique-parent-Directed-Graph →
+  no-direct-successor-root-unique-direct-successor-Directed-Graph :
+    unique-direct-successor-Directed-Graph →
     is-empty (Σ (vertex-Directed-Graph G) (edge-Directed-Graph G r))
-  no-parent-root-unique-parent-Directed-Graph H =
+  no-direct-successor-root-unique-direct-successor-Directed-Graph H =
     is-empty-right-summand-is-contr-coprod (H r) refl
 
-  is-isolated-root-unique-parent-Directed-Graph :
-    unique-parent-Directed-Graph → is-isolated r
-  is-isolated-root-unique-parent-Directed-Graph H x =
+  is-isolated-root-unique-direct-successor-Directed-Graph :
+    unique-direct-successor-Directed-Graph → is-isolated r
+  is-isolated-root-unique-direct-successor-Directed-Graph H x =
     map-coprod id (is-empty-left-summand-is-contr-coprod (H x)) (center (H x))
 
-  is-contr-walk-from-root-unique-parent-Directed-Graph :
-    unique-parent-Directed-Graph →
+  is-contr-walk-from-root-unique-direct-successor-Directed-Graph :
+    unique-direct-successor-Directed-Graph →
     is-contr (Σ (vertex-Directed-Graph G) (λ y → walk-Directed-Graph G r y))
-  pr1 (is-contr-walk-from-root-unique-parent-Directed-Graph H) =
+  pr1 (is-contr-walk-from-root-unique-direct-successor-Directed-Graph H) =
     ( r , refl-walk-Directed-Graph)
   pr2
-    ( is-contr-walk-from-root-unique-parent-Directed-Graph H)
+    ( is-contr-walk-from-root-unique-direct-successor-Directed-Graph H)
     ( y , refl-walk-Directed-Graph) =
     refl
   pr2
-    ( is-contr-walk-from-root-unique-parent-Directed-Graph H)
+    ( is-contr-walk-from-root-unique-direct-successor-Directed-Graph H)
     ( y , cons-walk-Directed-Graph e w) =
-    ex-falso (no-parent-root-unique-parent-Directed-Graph H (_ , e))
+    ex-falso
+      ( no-direct-successor-root-unique-direct-successor-Directed-Graph H
+        ( _ , e))
 
-  is-contr-loop-space-root-unique-parent-Directed-Graph :
-    unique-parent-Directed-Graph → is-contr (r ＝ r)
-  is-contr-loop-space-root-unique-parent-Directed-Graph H =
+  is-contr-loop-space-root-unique-direct-successor-Directed-Graph :
+    unique-direct-successor-Directed-Graph → is-contr (r ＝ r)
+  is-contr-loop-space-root-unique-direct-successor-Directed-Graph H =
     is-contr-loop-space-isolated-point r
-      ( is-isolated-root-unique-parent-Directed-Graph H)
+      ( is-isolated-root-unique-direct-successor-Directed-Graph H)
 
-  is-not-root-has-unique-parent-Directed-Graph :
+  is-not-root-has-unique-direct-successor-Directed-Graph :
     (x : vertex-Directed-Graph G) →
     is-contr
       ( (r ＝ x) + Σ (vertex-Directed-Graph G) (edge-Directed-Graph G x)) →
     Σ (vertex-Directed-Graph G) (edge-Directed-Graph G x) → ¬ (r ＝ x)
-  is-not-root-has-unique-parent-Directed-Graph x H (y , e) =
+  is-not-root-has-unique-direct-successor-Directed-Graph x H (y , e) =
     is-empty-left-summand-is-contr-coprod H (y , e)
 
-  is-proof-irrelevant-parent-has-unique-parent-Directed-Graph :
+  is-proof-irrelevant-direct-successor-has-unique-direct-successor-Directed-Graph :
     (x : vertex-Directed-Graph G) →
     is-contr
       ( (r ＝ x) + Σ (vertex-Directed-Graph G) (edge-Directed-Graph G x)) →
     is-proof-irrelevant (Σ (vertex-Directed-Graph G) (edge-Directed-Graph G x))
-  is-proof-irrelevant-parent-has-unique-parent-Directed-Graph x H (y , e) =
+  is-proof-irrelevant-direct-successor-has-unique-direct-successor-Directed-Graph
+    x H (y , e) =
     is-contr-right-summand H (y , e)
 
-  is-proof-irrelevant-walk-unique-parent-Directed-Graph :
-    unique-parent-Directed-Graph → (x : vertex-Directed-Graph G) →
+  is-proof-irrelevant-walk-unique-direct-successor-Directed-Graph :
+    unique-direct-successor-Directed-Graph → (x : vertex-Directed-Graph G) →
     is-proof-irrelevant (walk-Directed-Graph G x r)
   pr1
-    ( is-proof-irrelevant-walk-unique-parent-Directed-Graph H x
+    ( is-proof-irrelevant-walk-unique-direct-successor-Directed-Graph H x
       refl-walk-Directed-Graph) =
     refl-walk-Directed-Graph
   pr2
-    ( is-proof-irrelevant-walk-unique-parent-Directed-Graph H x
+    ( is-proof-irrelevant-walk-unique-direct-successor-Directed-Graph H x
       refl-walk-Directed-Graph)
     ( w) =
     ( inv
       ( ap
         ( λ α → tr (walk-Directed-Graph G x) α refl-walk-Directed-Graph)
         ( eq-is-contr
-          ( is-contr-loop-space-root-unique-parent-Directed-Graph H)))) ∙
+          ( is-contr-loop-space-root-unique-direct-successor-Directed-Graph
+            ( H))))) ∙
     ( pr2
       ( pair-eq-Σ
         ( eq-is-contr
-          ( is-contr-walk-from-root-unique-parent-Directed-Graph H)
+          ( is-contr-walk-from-root-unique-direct-successor-Directed-Graph H)
           { (r , refl-walk-Directed-Graph)}
           { (r , w)})))
-  is-proof-irrelevant-walk-unique-parent-Directed-Graph H x
+  is-proof-irrelevant-walk-unique-direct-successor-Directed-Graph H x
     ( cons-walk-Directed-Graph {.x} {y} e w) =
     is-contr-equiv
       ( walk-Directed-Graph G y r)
@@ -456,7 +464,9 @@ module _
             ( Σ ( vertex-Directed-Graph G)
                 ( λ y →
                   edge-Directed-Graph G x y × walk-Directed-Graph G y r))
-            ( is-not-root-has-unique-parent-Directed-Graph x (H x) (y , e))
+            ( is-not-root-has-unique-direct-successor-Directed-Graph x
+              ( H x)
+              ( y , e))
         ≃ Σ ( Σ (vertex-Directed-Graph G) (edge-Directed-Graph G x))
             ( λ p → walk-Directed-Graph G (pr1 p) r)
           by
@@ -467,75 +477,80 @@ module _
         ≃ walk-Directed-Graph G y r
           by
           left-unit-law-Σ-is-contr
-            ( is-proof-irrelevant-parent-has-unique-parent-Directed-Graph x
+            ( is-proof-irrelevant-direct-successor-has-unique-direct-successor-Directed-Graph
+              ( x)
               ( H x)
               ( y , e))
             (y , e))
-      ( is-proof-irrelevant-walk-unique-parent-Directed-Graph H y w)
+      ( is-proof-irrelevant-walk-unique-direct-successor-Directed-Graph H y w)
 
-  is-tree-unique-parent-Directed-Graph' :
-    unique-parent-Directed-Graph →
+  is-tree-unique-direct-successor-Directed-Graph' :
+    unique-direct-successor-Directed-Graph →
     ((x : vertex-Directed-Graph G) → walk-Directed-Graph G x r) →
     is-tree-Directed-Graph' G r
-  is-tree-unique-parent-Directed-Graph' H w x =
-    is-proof-irrelevant-walk-unique-parent-Directed-Graph H x (w x)
+  is-tree-unique-direct-successor-Directed-Graph' H w x =
+    is-proof-irrelevant-walk-unique-direct-successor-Directed-Graph H x (w x)
 
-  is-tree-unique-parent-Directed-Graph :
-    unique-parent-Directed-Graph →
+  is-tree-unique-direct-successor-Directed-Graph :
+    unique-direct-successor-Directed-Graph →
     ((x : vertex-Directed-Graph G) → walk-Directed-Graph G x r) →
     is-tree-Directed-Graph G
-  pr1 (is-tree-unique-parent-Directed-Graph H w) = r
-  pr2 (is-tree-unique-parent-Directed-Graph H w) =
-    is-tree-unique-parent-Directed-Graph' H w
+  pr1 (is-tree-unique-direct-successor-Directed-Graph H w) = r
+  pr2 (is-tree-unique-direct-successor-Directed-Graph H w) =
+    is-tree-unique-direct-successor-Directed-Graph' H w
 ```
 
-### Nodes in trees have unique parents
+### Nodes in trees have unique direct-successors
 
 ```agda
 module _
   {l1 l2 : Level} (T : Directed-Tree l1 l2)
   where
 
-  center-walk-unique-parent-Directed-Tree :
+  center-walk-unique-direct-successor-Directed-Tree :
     (x : node-Directed-Tree T)
     (w : walk-Directed-Tree T x (root-Directed-Tree T)) →
     is-root-Directed-Tree T x +
     Σ (node-Directed-Tree T) (edge-Directed-Tree T x)
-  center-walk-unique-parent-Directed-Tree .(root-Directed-Tree T)
+  center-walk-unique-direct-successor-Directed-Tree .(root-Directed-Tree T)
     refl-walk-Directed-Graph =
     inl refl
-  center-walk-unique-parent-Directed-Tree x
+  center-walk-unique-direct-successor-Directed-Tree x
     ( cons-walk-Directed-Graph {.x} {y} e w) =
     inr (y , e)
 
-  center-unique-parent-Directed-Tree :
+  center-unique-direct-successor-Directed-Tree :
     (x : node-Directed-Tree T) →
     is-root-Directed-Tree T x +
     Σ (node-Directed-Tree T) (edge-Directed-Tree T x)
-  center-unique-parent-Directed-Tree x =
-    center-walk-unique-parent-Directed-Tree x (walk-to-root-Directed-Tree T x)
+  center-unique-direct-successor-Directed-Tree x =
+    center-walk-unique-direct-successor-Directed-Tree x
+      ( walk-to-root-Directed-Tree T x)
 
-  contraction-walk-unique-parent-Directed-Tree :
+  contraction-walk-unique-direct-successor-Directed-Tree :
     (x : node-Directed-Tree T)
     (w : walk-Directed-Tree T x (root-Directed-Tree T)) →
     (p : is-root-Directed-Tree T x +
          Σ (node-Directed-Tree T) (edge-Directed-Tree T x)) →
-    center-walk-unique-parent-Directed-Tree x w ＝ p
-  contraction-walk-unique-parent-Directed-Tree ._ refl-walk-Directed-Graph
-    ( inl p) = ap inl (eq-refl-root-Directed-Tree' T p)
-  contraction-walk-unique-parent-Directed-Tree ._ refl-walk-Directed-Graph
+    center-walk-unique-direct-successor-Directed-Tree x w ＝ p
+  contraction-walk-unique-direct-successor-Directed-Tree ._
+    ( refl-walk-Directed-Graph)
+    ( inl p) =
+    ap inl (eq-refl-root-Directed-Tree' T p)
+  contraction-walk-unique-direct-successor-Directed-Tree ._
+    ( refl-walk-Directed-Graph)
     ( inr (y , e)) =
-    ex-falso (no-parent-root-Directed-Tree T (y , e))
-  contraction-walk-unique-parent-Directed-Tree _
+    ex-falso (no-direct-successor-root-Directed-Tree T (y , e))
+  contraction-walk-unique-direct-successor-Directed-Tree _
     ( cons-walk-Directed-Graph {._} {y} e w)
     ( inl refl) =
-    ex-falso (no-parent-root-Directed-Tree T (y , e))
-  contraction-walk-unique-parent-Directed-Tree _
+    ex-falso (no-direct-successor-root-Directed-Tree T (y , e))
+  contraction-walk-unique-direct-successor-Directed-Tree _
     ( cons-walk-Directed-Graph {x} {y} e w)
     ( inr (z , f)) =
     ap
       ( inr)
-      ( eq-parent-eq-cons-walk-Directed-Graph
+      ( eq-direct-successor-eq-cons-walk-Directed-Graph
         ( graph-Directed-Tree T)
         ( x)
         ( e)
@@ -544,26 +559,28 @@ module _
         ( walk-to-root-Directed-Tree T z)
         ( eq-is-contr (unique-walk-to-root-Directed-Tree T x)))
 
-  contraction-unique-parent-Directed-Tree :
+  contraction-unique-direct-successor-Directed-Tree :
     (x : node-Directed-Tree T) →
     (p : is-root-Directed-Tree T x +
          Σ (node-Directed-Tree T) (edge-Directed-Tree T x)) →
-    center-unique-parent-Directed-Tree x ＝ p
-  contraction-unique-parent-Directed-Tree x =
-    contraction-walk-unique-parent-Directed-Tree x
+    center-unique-direct-successor-Directed-Tree x ＝ p
+  contraction-unique-direct-successor-Directed-Tree x =
+    contraction-walk-unique-direct-successor-Directed-Tree x
       ( walk-to-root-Directed-Tree T x)
 
-  unique-parent-Directed-Tree :
-    unique-parent-Directed-Graph (graph-Directed-Tree T) (root-Directed-Tree T)
-  pr1 (unique-parent-Directed-Tree x) =
-    center-unique-parent-Directed-Tree x
-  pr2 (unique-parent-Directed-Tree x) =
-    contraction-unique-parent-Directed-Tree x
+  unique-direct-successor-Directed-Tree :
+    unique-direct-successor-Directed-Graph
+      ( graph-Directed-Tree T)
+      ( root-Directed-Tree T)
+  pr1 (unique-direct-successor-Directed-Tree x) =
+    center-unique-direct-successor-Directed-Tree x
+  pr2 (unique-direct-successor-Directed-Tree x) =
+    contraction-unique-direct-successor-Directed-Tree x
 
-  unique-parent-is-proper-node-Directed-Tree :
+  unique-direct-successor-is-proper-node-Directed-Tree :
     (x : node-Directed-Tree T) → is-proper-node-Directed-Tree T x →
     is-contr (Σ (node-Directed-Tree T) (edge-Directed-Tree T x))
-  unique-parent-is-proper-node-Directed-Tree x f =
+  unique-direct-successor-is-proper-node-Directed-Tree x f =
     is-contr-equiv'
       ( ( is-root-Directed-Tree T x) +
         ( Σ (node-Directed-Tree T) (edge-Directed-Tree T x)))
@@ -571,32 +588,33 @@ module _
         ( is-root-Directed-Tree T x)
         ( Σ (node-Directed-Tree T) (edge-Directed-Tree T x))
         ( f))
-      ( unique-parent-Directed-Tree x)
+      ( unique-direct-successor-Directed-Tree x)
 
-  is-proof-irrelevant-parent-Directed-Tree :
+  is-proof-irrelevant-direct-successor-Directed-Tree :
     (x : node-Directed-Tree T) →
     is-proof-irrelevant (Σ (node-Directed-Tree T) (edge-Directed-Tree T x))
-  is-proof-irrelevant-parent-Directed-Tree x (y , e) =
-    unique-parent-is-proper-node-Directed-Tree x
-      ( λ { refl → no-parent-root-Directed-Tree T (y , e)})
+  is-proof-irrelevant-direct-successor-Directed-Tree x (y , e) =
+    unique-direct-successor-is-proper-node-Directed-Tree x
+      ( λ { refl → no-direct-successor-root-Directed-Tree T (y , e)})
 
-  is-prop-parent-Directed-Tree :
+  is-prop-direct-successor-Directed-Tree :
     (x : node-Directed-Tree T) →
     is-prop (Σ (node-Directed-Tree T) (edge-Directed-Tree T x))
-  is-prop-parent-Directed-Tree x =
-    is-prop-is-proof-irrelevant (is-proof-irrelevant-parent-Directed-Tree x)
+  is-prop-direct-successor-Directed-Tree x =
+    is-prop-is-proof-irrelevant
+      ( is-proof-irrelevant-direct-successor-Directed-Tree x)
 
-  eq-parent-Directed-Tree :
+  eq-direct-successor-Directed-Tree :
     {x : node-Directed-Tree T}
     (u v : Σ (node-Directed-Tree T) (edge-Directed-Tree T x)) → u ＝ v
-  eq-parent-Directed-Tree {x} =
-    eq-is-prop' (is-prop-parent-Directed-Tree x)
+  eq-direct-successor-Directed-Tree {x} =
+    eq-is-prop' (is-prop-direct-successor-Directed-Tree x)
 
-  parent-is-proper-node-Directed-Tree :
+  direct-successor-is-proper-node-Directed-Tree :
     (x : node-Directed-Tree T) → is-proper-node-Directed-Tree T x →
     Σ (node-Directed-Tree T) (edge-Directed-Tree T x)
-  parent-is-proper-node-Directed-Tree x f =
-    center (unique-parent-is-proper-node-Directed-Tree x f)
+  direct-successor-is-proper-node-Directed-Tree x f =
+    center (unique-direct-successor-is-proper-node-Directed-Tree x f)
 ```
 
 ### Transporting walks in directed trees
@@ -606,16 +624,16 @@ module _
   {l1 l2 : Level} (T : Directed-Tree l1 l2)
   where
 
-  tr-walk-eq-parent-Directed-Tree :
+  tr-walk-eq-direct-successor-Directed-Tree :
     {x y : node-Directed-Tree T}
     (u v : Σ (node-Directed-Tree T) (edge-Directed-Tree T x)) →
     walk-Directed-Tree T (pr1 u) y → walk-Directed-Tree T (pr1 v) y
-  tr-walk-eq-parent-Directed-Tree {x} {y} u v =
+  tr-walk-eq-direct-successor-Directed-Tree {x} {y} u v =
     tr
       ( λ r → walk-Directed-Tree T (pr1 r) y)
-      ( eq-parent-Directed-Tree T u v)
+      ( eq-direct-successor-Directed-Tree T u v)
 
-  eq-tr-walk-eq-parent-Directed-Tree' :
+  eq-tr-walk-eq-direct-successor-Directed-Tree' :
     {x y : node-Directed-Tree T}
     (u v : Σ (node-Directed-Tree T) (edge-Directed-Tree T x)) →
     (w : walk-Directed-Tree T (pr1 u) y) →
@@ -624,16 +642,19 @@ module _
       ( pr2 v)
       ( tr (λ r → walk-Directed-Tree T (pr1 r) y) p w) ＝
     cons-walk-Directed-Graph (pr2 u) w
-  eq-tr-walk-eq-parent-Directed-Tree' u .u w refl = refl
+  eq-tr-walk-eq-direct-successor-Directed-Tree' u .u w refl = refl
 
-  eq-tr-walk-eq-parent-Directed-Tree :
+  eq-tr-walk-eq-direct-successor-Directed-Tree :
     {x y : node-Directed-Tree T}
     (u v : Σ (node-Directed-Tree T) (edge-Directed-Tree T x)) →
     (w : walk-Directed-Tree T (pr1 u) y) →
-    cons-walk-Directed-Graph (pr2 v) (tr-walk-eq-parent-Directed-Tree u v w) ＝
+    cons-walk-Directed-Graph
+      ( pr2 v)
+      ( tr-walk-eq-direct-successor-Directed-Tree u v w) ＝
     cons-walk-Directed-Graph (pr2 u) w
-  eq-tr-walk-eq-parent-Directed-Tree u v w =
-    eq-tr-walk-eq-parent-Directed-Tree' u v w (eq-parent-Directed-Tree T u v)
+  eq-tr-walk-eq-direct-successor-Directed-Tree u v w =
+    eq-tr-walk-eq-direct-successor-Directed-Tree' u v w
+      ( eq-direct-successor-Directed-Tree T u v)
 ```
 
 ## See also
diff --git a/src/trees/enriched-directed-trees.lagda.md b/src/trees/enriched-directed-trees.lagda.md
index 89c04868dd..8fdfc30df1 100644
--- a/src/trees/enriched-directed-trees.lagda.md
+++ b/src/trees/enriched-directed-trees.lagda.md
@@ -82,22 +82,25 @@ module _
   edge-Enriched-Directed-Tree =
     edge-Directed-Tree directed-tree-Enriched-Directed-Tree
 
-  children-Enriched-Directed-Tree :
+  direct-predecessor-Enriched-Directed-Tree :
     node-Enriched-Directed-Tree → UU (l3 ⊔ l4)
-  children-Enriched-Directed-Tree =
-    children-Directed-Tree directed-tree-Enriched-Directed-Tree
+  direct-predecessor-Enriched-Directed-Tree =
+    direct-predecessor-Directed-Tree directed-tree-Enriched-Directed-Tree
 
-  node-children-Enriched-Directed-Tree :
+  node-direct-predecessor-Enriched-Directed-Tree :
     (x : node-Enriched-Directed-Tree) →
-    children-Enriched-Directed-Tree x → node-Enriched-Directed-Tree
-  node-children-Enriched-Directed-Tree =
-    node-children-Directed-Tree directed-tree-Enriched-Directed-Tree
-
-  edge-children-Enriched-Directed-Tree :
-    (x : node-Enriched-Directed-Tree) (y : children-Enriched-Directed-Tree x) →
-    edge-Enriched-Directed-Tree (node-children-Enriched-Directed-Tree x y) x
-  edge-children-Enriched-Directed-Tree =
-    edge-children-Directed-Tree directed-tree-Enriched-Directed-Tree
+    direct-predecessor-Enriched-Directed-Tree x → node-Enriched-Directed-Tree
+  node-direct-predecessor-Enriched-Directed-Tree =
+    node-direct-predecessor-Directed-Tree directed-tree-Enriched-Directed-Tree
+
+  edge-direct-predecessor-Enriched-Directed-Tree :
+    (x : node-Enriched-Directed-Tree)
+    (y : direct-predecessor-Enriched-Directed-Tree x) →
+    edge-Enriched-Directed-Tree
+      ( node-direct-predecessor-Enriched-Directed-Tree x y)
+      ( x)
+  edge-direct-predecessor-Enriched-Directed-Tree =
+    edge-direct-predecessor-Directed-Tree directed-tree-Enriched-Directed-Tree
 
   walk-Enriched-Directed-Tree :
     (x y : node-Enriched-Directed-Tree) → UU (l3 ⊔ l4)
@@ -173,17 +176,18 @@ module _
   eq-refl-root-Enriched-Directed-Tree' =
     eq-refl-root-Directed-Tree' directed-tree-Enriched-Directed-Tree
 
-  no-parent-root-Enriched-Directed-Tree :
+  no-direct-successor-root-Enriched-Directed-Tree :
     ¬ ( Σ ( node-Enriched-Directed-Tree)
           ( edge-Enriched-Directed-Tree root-Enriched-Directed-Tree))
-  no-parent-root-Enriched-Directed-Tree =
-    no-parent-root-Directed-Tree directed-tree-Enriched-Directed-Tree
+  no-direct-successor-root-Enriched-Directed-Tree =
+    no-direct-successor-root-Directed-Tree directed-tree-Enriched-Directed-Tree
 
-  is-proper-node-parent-Enriched-Directed-Tree :
+  is-proper-node-direct-successor-Enriched-Directed-Tree :
     {x y : node-Enriched-Directed-Tree} (e : edge-Enriched-Directed-Tree x y) →
     ¬ (is-root-Enriched-Directed-Tree x)
-  is-proper-node-parent-Enriched-Directed-Tree =
-    is-proper-node-parent-Directed-Tree directed-tree-Enriched-Directed-Tree
+  is-proper-node-direct-successor-Enriched-Directed-Tree =
+    is-proper-node-direct-successor-Directed-Tree
+      directed-tree-Enriched-Directed-Tree
 
   is-proof-irrelevant-edge-to-root-Enriched-Directed-Tree :
     (x : node-Enriched-Directed-Tree) →
@@ -223,49 +227,50 @@ module _
   walk-to-root-Enriched-Directed-Tree =
     walk-to-root-Directed-Tree directed-tree-Enriched-Directed-Tree
 
-  unique-parent-Enriched-Directed-Tree :
-    unique-parent-Directed-Graph
+  unique-direct-successor-Enriched-Directed-Tree :
+    unique-direct-successor-Directed-Graph
       graph-Enriched-Directed-Tree
       root-Enriched-Directed-Tree
-  unique-parent-Enriched-Directed-Tree =
-    unique-parent-Directed-Tree directed-tree-Enriched-Directed-Tree
+  unique-direct-successor-Enriched-Directed-Tree =
+    unique-direct-successor-Directed-Tree directed-tree-Enriched-Directed-Tree
 
-  unique-parent-is-proper-node-Enriched-Directed-Tree :
+  unique-direct-successor-is-proper-node-Enriched-Directed-Tree :
     (x : node-Enriched-Directed-Tree) →
     is-proper-node-Enriched-Directed-Tree x →
     is-contr ( Σ node-Enriched-Directed-Tree (edge-Enriched-Directed-Tree x))
-  unique-parent-is-proper-node-Enriched-Directed-Tree =
-    unique-parent-is-proper-node-Directed-Tree
+  unique-direct-successor-is-proper-node-Enriched-Directed-Tree =
+    unique-direct-successor-is-proper-node-Directed-Tree
       directed-tree-Enriched-Directed-Tree
 
-  is-proof-irrelevant-parent-Enriched-Directed-Tree :
+  is-proof-irrelevant-direct-successor-Enriched-Directed-Tree :
     (x : node-Enriched-Directed-Tree) →
     is-proof-irrelevant
       ( Σ (node-Enriched-Directed-Tree) (edge-Enriched-Directed-Tree x))
-  is-proof-irrelevant-parent-Enriched-Directed-Tree =
-    is-proof-irrelevant-parent-Directed-Tree
+  is-proof-irrelevant-direct-successor-Enriched-Directed-Tree =
+    is-proof-irrelevant-direct-successor-Directed-Tree
       directed-tree-Enriched-Directed-Tree
 
-  is-prop-parent-Enriched-Directed-Tree :
+  is-prop-direct-successor-Enriched-Directed-Tree :
     (x : node-Enriched-Directed-Tree) →
     is-prop
       ( Σ (node-Enriched-Directed-Tree) (edge-Enriched-Directed-Tree x))
-  is-prop-parent-Enriched-Directed-Tree =
-    is-prop-parent-Directed-Tree directed-tree-Enriched-Directed-Tree
+  is-prop-direct-successor-Enriched-Directed-Tree =
+    is-prop-direct-successor-Directed-Tree directed-tree-Enriched-Directed-Tree
 
-  eq-parent-Enriched-Directed-Tree :
+  eq-direct-successor-Enriched-Directed-Tree :
     {x : node-Enriched-Directed-Tree}
     ( u v : Σ (node-Enriched-Directed-Tree) (edge-Enriched-Directed-Tree x)) →
     u ＝ v
-  eq-parent-Enriched-Directed-Tree =
-    eq-parent-Directed-Tree directed-tree-Enriched-Directed-Tree
+  eq-direct-successor-Enriched-Directed-Tree =
+    eq-direct-successor-Directed-Tree directed-tree-Enriched-Directed-Tree
 
-  parent-is-proper-node-Enriched-Directed-Tree :
+  direct-successor-is-proper-node-Enriched-Directed-Tree :
     (x : node-Enriched-Directed-Tree) →
     ¬ (is-root-Enriched-Directed-Tree x) →
     Σ (node-Enriched-Directed-Tree) (edge-Enriched-Directed-Tree x)
-  parent-is-proper-node-Enriched-Directed-Tree =
-    parent-is-proper-node-Directed-Tree directed-tree-Enriched-Directed-Tree
+  direct-successor-is-proper-node-Enriched-Directed-Tree =
+    direct-successor-is-proper-node-Directed-Tree
+      directed-tree-Enriched-Directed-Tree
 
   shape-Enriched-Directed-Tree : node-Enriched-Directed-Tree → A
   shape-Enriched-Directed-Tree = pr1 (pr2 T)
@@ -282,7 +287,8 @@ module _
 
   map-enrichment-Enriched-Directed-Tree :
     (x : node-Enriched-Directed-Tree) →
-    B (shape-Enriched-Directed-Tree x) → children-Enriched-Directed-Tree x
+    B (shape-Enriched-Directed-Tree x) →
+    direct-predecessor-Enriched-Directed-Tree x
   map-enrichment-Enriched-Directed-Tree x =
     map-equiv (enrichment-Enriched-Directed-Tree x)
 
diff --git a/src/trees/equivalences-directed-trees.lagda.md b/src/trees/equivalences-directed-trees.lagda.md
index 55d69e5462..0bd7ed82a4 100644
--- a/src/trees/equivalences-directed-trees.lagda.md
+++ b/src/trees/equivalences-directed-trees.lagda.md
@@ -178,24 +178,24 @@ module _
       ( graph-Directed-Tree T)
       ( e)
 
-  equiv-children-equiv-Directed-Tree :
+  equiv-direct-predecessor-equiv-Directed-Tree :
     (x : node-Directed-Tree S) →
     ( Σ (node-Directed-Tree S) (λ y → edge-Directed-Tree S y x)) ≃
     ( Σ ( node-Directed-Tree T)
         ( λ y → edge-Directed-Tree T y (node-equiv-Directed-Tree x)))
-  equiv-children-equiv-Directed-Tree x =
+  equiv-direct-predecessor-equiv-Directed-Tree x =
     equiv-Σ
       ( λ y → edge-Directed-Tree T y (node-equiv-Directed-Tree x))
       ( equiv-node-equiv-Directed-Tree)
       ( λ y → equiv-edge-equiv-Directed-Tree y x)
 
-  children-equiv-Directed-Tree :
+  direct-predecessor-equiv-Directed-Tree :
     (x : node-Directed-Tree S) →
     Σ (node-Directed-Tree S) (λ y → edge-Directed-Tree S y x) →
     Σ ( node-Directed-Tree T)
       ( λ y → edge-Directed-Tree T y (node-equiv-Directed-Tree x))
-  children-equiv-Directed-Tree x =
-    map-equiv (equiv-children-equiv-Directed-Tree x)
+  direct-predecessor-equiv-Directed-Tree x =
+    map-equiv (equiv-direct-predecessor-equiv-Directed-Tree x)
 
   equiv-walk-equiv-Directed-Tree :
     {x y : node-Directed-Tree S} →
@@ -466,15 +466,15 @@ module _
   ... | inl refl =
     is-equiv-is-empty _
       ( λ u →
-        no-parent-root-Directed-Tree T
+        no-direct-successor-root-Directed-Tree T
           ( tr
             ( λ v → Σ (node-Directed-Tree T) (edge-Directed-Tree T v))
             ( inv (preserves-root-is-equiv-node-hom-Directed-Tree S T f H))
             ( u)))
   ... | inr p =
     is-equiv-is-contr _
-      ( unique-parent-is-proper-node-Directed-Tree S x p)
-      ( unique-parent-is-proper-node-Directed-Tree T
+      ( unique-direct-successor-is-proper-node-Directed-Tree S x p)
+      ( unique-direct-successor-is-proper-node-Directed-Tree T
         ( node-hom-Directed-Tree S T f x)
         ( is-not-root-node-hom-is-not-root-Directed-Tree S T f x p))
 
diff --git a/src/trees/equivalences-enriched-directed-trees.lagda.md b/src/trees/equivalences-enriched-directed-trees.lagda.md
index 16ae414be8..192269bd73 100644
--- a/src/trees/equivalences-enriched-directed-trees.lagda.md
+++ b/src/trees/equivalences-enriched-directed-trees.lagda.md
@@ -90,7 +90,7 @@ equiv-Enriched-Directed-Tree A B S T =
         ( λ H →
           (x : node-Enriched-Directed-Tree A B S) →
           htpy-equiv
-            ( ( equiv-children-equiv-Directed-Tree
+            ( ( equiv-direct-predecessor-equiv-Directed-Tree
                 ( directed-tree-Enriched-Directed-Tree A B S)
                 ( directed-tree-Enriched-Directed-Tree A B T)
                 ( e)
@@ -184,7 +184,7 @@ module _
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( equiv-directed-tree-equiv-Enriched-Directed-Tree)
 
-  equiv-children-equiv-Enriched-Directed-Tree :
+  equiv-direct-predecessor-equiv-Enriched-Directed-Tree :
     ( x : node-Enriched-Directed-Tree A B S) →
     Σ ( node-Enriched-Directed-Tree A B S)
       ( λ y → edge-Enriched-Directed-Tree A B S y x) ≃
@@ -192,13 +192,13 @@ module _
       ( λ y →
         edge-Enriched-Directed-Tree A B T y
           ( node-equiv-Enriched-Directed-Tree x))
-  equiv-children-equiv-Enriched-Directed-Tree =
-    equiv-children-equiv-Directed-Tree
+  equiv-direct-predecessor-equiv-Enriched-Directed-Tree =
+    equiv-direct-predecessor-equiv-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B S)
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( equiv-directed-tree-equiv-Enriched-Directed-Tree)
 
-  children-equiv-Enriched-Directed-Tree :
+  direct-predecessor-equiv-Enriched-Directed-Tree :
     ( x : node-Enriched-Directed-Tree A B S) →
     Σ ( node-Enriched-Directed-Tree A B S)
       ( λ y → edge-Enriched-Directed-Tree A B S y x) →
@@ -206,8 +206,8 @@ module _
       ( λ y →
         edge-Enriched-Directed-Tree A B T y
           ( node-equiv-Enriched-Directed-Tree x))
-  children-equiv-Enriched-Directed-Tree =
-    children-equiv-Directed-Tree
+  direct-predecessor-equiv-Enriched-Directed-Tree =
+    direct-predecessor-equiv-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B S)
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( equiv-directed-tree-equiv-Enriched-Directed-Tree)
@@ -219,7 +219,7 @@ module _
 
   enrichment-equiv-Enriched-Directed-Tree :
     ( x : node-Enriched-Directed-Tree A B S) →
-    ( ( children-equiv-Enriched-Directed-Tree x) ∘
+    ( ( direct-predecessor-equiv-Enriched-Directed-Tree x) ∘
       ( map-enrichment-Enriched-Directed-Tree A B S x)) ~
     ( ( map-enrichment-Enriched-Directed-Tree A B T
         ( node-equiv-Directed-Tree
@@ -335,24 +335,24 @@ module _
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( equiv-directed-tree-comp-equiv-Enriched-Directed-Tree)
 
-  equiv-children-comp-equiv-Enriched-Directed-Tree :
+  equiv-direct-predecessor-comp-equiv-Enriched-Directed-Tree :
     (x : node-Enriched-Directed-Tree A B R) →
-    children-Enriched-Directed-Tree A B R x ≃
-    children-Enriched-Directed-Tree A B T
+    direct-predecessor-Enriched-Directed-Tree A B R x ≃
+    direct-predecessor-Enriched-Directed-Tree A B T
       ( node-comp-equiv-Enriched-Directed-Tree x)
-  equiv-children-comp-equiv-Enriched-Directed-Tree =
-    equiv-children-equiv-Directed-Tree
+  equiv-direct-predecessor-comp-equiv-Enriched-Directed-Tree =
+    equiv-direct-predecessor-equiv-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B R)
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( equiv-directed-tree-comp-equiv-Enriched-Directed-Tree)
 
-  children-comp-equiv-Enriched-Directed-Tree :
+  direct-predecessor-comp-equiv-Enriched-Directed-Tree :
     (x : node-Enriched-Directed-Tree A B R) →
-    children-Enriched-Directed-Tree A B R x →
-    children-Enriched-Directed-Tree A B T
+    direct-predecessor-Enriched-Directed-Tree A B R x →
+    direct-predecessor-Enriched-Directed-Tree A B T
       ( node-comp-equiv-Enriched-Directed-Tree x)
-  children-comp-equiv-Enriched-Directed-Tree =
-    children-equiv-Directed-Tree
+  direct-predecessor-comp-equiv-Enriched-Directed-Tree =
+    direct-predecessor-equiv-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B R)
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( equiv-directed-tree-comp-equiv-Enriched-Directed-Tree)
@@ -378,7 +378,7 @@ module _
       ( map-enrichment-Enriched-Directed-Tree A B R x)
       ( map-enrichment-Enriched-Directed-Tree A B T
         ( node-comp-equiv-Enriched-Directed-Tree x))
-      ( children-comp-equiv-Enriched-Directed-Tree x)
+      ( direct-predecessor-comp-equiv-Enriched-Directed-Tree x)
   enrichment-comp-equiv-Enriched-Directed-Tree x =
     pasting-horizontal-up-to-htpy-coherence-square-maps
       ( tr B (shape-equiv-Enriched-Directed-Tree A B R S f x))
@@ -390,8 +390,8 @@ module _
         ( node-equiv-Enriched-Directed-Tree A B R S f x))
       ( map-enrichment-Enriched-Directed-Tree A B T
         ( node-comp-equiv-Enriched-Directed-Tree x))
-      ( children-equiv-Enriched-Directed-Tree A B R S f x)
-      ( children-equiv-Enriched-Directed-Tree A B S T g
+      ( direct-predecessor-equiv-Enriched-Directed-Tree A B R S f x)
+      ( direct-predecessor-equiv-Enriched-Directed-Tree A B S T g
         ( node-equiv-Enriched-Directed-Tree A B R S f x))
       ( tr-concat
         ( shape-equiv-Enriched-Directed-Tree A B R S f x)
@@ -450,7 +450,7 @@ module _
                 ( e))))
           ( λ H →
             ( x : node-Enriched-Directed-Tree A B T) →
-            ( ( children-equiv-Directed-Tree
+            ( ( direct-predecessor-equiv-Directed-Tree
                 ( directed-tree-Enriched-Directed-Tree A B T)
                 ( S)
                 ( e)
diff --git a/src/trees/fibers-directed-trees.lagda.md b/src/trees/fibers-directed-trees.lagda.md
index a48893f9c6..6f456c405a 100644
--- a/src/trees/fibers-directed-trees.lagda.md
+++ b/src/trees/fibers-directed-trees.lagda.md
@@ -20,6 +20,7 @@ open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels
 
 open import graph-theory.directed-graphs
+open import graph-theory.fibers-directed-graphs
 open import graph-theory.walks-directed-graphs
 
 open import trees.bases-directed-trees
@@ -46,127 +47,108 @@ module _
 
   node-fiber-Directed-Tree : UU (l1 ⊔ l2)
   node-fiber-Directed-Tree =
-    Σ (node-Directed-Tree T) (λ y → walk-Directed-Tree T y x)
+    node-fiber-Directed-Graph (graph-Directed-Tree T) x
 
-  module _
-    (u : node-fiber-Directed-Tree)
-    where
+  node-inclusion-fiber-Directed-Tree :
+    node-fiber-Directed-Tree → node-Directed-Tree T
+  node-inclusion-fiber-Directed-Tree =
+    node-inclusion-fiber-Directed-Graph (graph-Directed-Tree T) x
 
-    node-inclusion-fiber-Directed-Tree : node-Directed-Tree T
-    node-inclusion-fiber-Directed-Tree = pr1 u
-
-    walk-node-inclusion-fiber-Directed-Tree :
-      walk-Directed-Tree T node-inclusion-fiber-Directed-Tree x
-    walk-node-inclusion-fiber-Directed-Tree = pr2 u
+  walk-node-inclusion-fiber-Directed-Tree :
+    (y : node-fiber-Directed-Tree) →
+    walk-Directed-Tree T (node-inclusion-fiber-Directed-Tree y) x
+  walk-node-inclusion-fiber-Directed-Tree =
+    walk-node-inclusion-fiber-Directed-Graph (graph-Directed-Tree T) x
 
   root-fiber-Directed-Tree : node-fiber-Directed-Tree
-  pr1 root-fiber-Directed-Tree = x
-  pr2 root-fiber-Directed-Tree = refl-walk-Directed-Tree T
+  root-fiber-Directed-Tree =
+    root-fiber-Directed-Graph (graph-Directed-Tree T) x
 
   is-root-fiber-Directed-Tree : node-fiber-Directed-Tree → UU (l1 ⊔ l2)
-  is-root-fiber-Directed-Tree y = root-fiber-Directed-Tree ＝ y
+  is-root-fiber-Directed-Tree =
+    is-root-fiber-Directed-Graph (graph-Directed-Tree T) x
 
   edge-fiber-Directed-Tree : (y z : node-fiber-Directed-Tree) → UU (l1 ⊔ l2)
-  edge-fiber-Directed-Tree y z =
-    Σ ( edge-Directed-Tree T
-        ( node-inclusion-fiber-Directed-Tree y)
-        ( node-inclusion-fiber-Directed-Tree z))
-      ( λ e →
-        ( walk-node-inclusion-fiber-Directed-Tree y) ＝
-        ( cons-walk-Directed-Tree T e
-          ( walk-node-inclusion-fiber-Directed-Tree z)))
-
-  module _
-    (y z : node-fiber-Directed-Tree) (e : edge-fiber-Directed-Tree y z)
-    where
-
-    edge-inclusion-fiber-Directed-Tree :
-      edge-Directed-Tree T
-        ( node-inclusion-fiber-Directed-Tree y)
-        ( node-inclusion-fiber-Directed-Tree z)
-    edge-inclusion-fiber-Directed-Tree = pr1 e
-
-    walk-edge-fiber-Directed-Tree :
-      walk-node-inclusion-fiber-Directed-Tree y ＝
-      cons-walk-Directed-Tree T
-        ( edge-inclusion-fiber-Directed-Tree)
-        ( walk-node-inclusion-fiber-Directed-Tree z)
-    walk-edge-fiber-Directed-Tree = pr2 e
+  edge-fiber-Directed-Tree =
+    edge-fiber-Directed-Graph (graph-Directed-Tree T) x
+
+  edge-inclusion-fiber-Directed-Tree :
+    (y z : node-fiber-Directed-Tree) (e : edge-fiber-Directed-Tree y z) →
+    edge-Directed-Tree T
+      ( node-inclusion-fiber-Directed-Tree y)
+      ( node-inclusion-fiber-Directed-Tree z)
+  edge-inclusion-fiber-Directed-Tree =
+    edge-inclusion-fiber-Directed-Graph (graph-Directed-Tree T) x
+
+  walk-edge-fiber-Directed-Tree :
+    (y z : node-fiber-Directed-Tree) (e : edge-fiber-Directed-Tree y z) →
+    walk-node-inclusion-fiber-Directed-Tree y ＝
+    cons-walk-Directed-Tree T
+      ( edge-inclusion-fiber-Directed-Tree y z e)
+      ( walk-node-inclusion-fiber-Directed-Tree z)
+  walk-edge-fiber-Directed-Tree =
+    walk-edge-fiber-Directed-Graph (graph-Directed-Tree T) x
 
   graph-fiber-Directed-Tree : Directed-Graph (l1 ⊔ l2) (l1 ⊔ l2)
-  pr1 graph-fiber-Directed-Tree = node-fiber-Directed-Tree
-  pr2 graph-fiber-Directed-Tree = edge-fiber-Directed-Tree
+  graph-fiber-Directed-Tree =
+    graph-fiber-Directed-Graph (graph-Directed-Tree T) x
 
   walk-fiber-Directed-Tree : (y z : node-fiber-Directed-Tree) → UU (l1 ⊔ l2)
-  walk-fiber-Directed-Tree = walk-Directed-Graph graph-fiber-Directed-Tree
+  walk-fiber-Directed-Tree =
+    walk-fiber-Directed-Graph (graph-Directed-Tree T) x
 
   walk-to-root-fiber-walk-Directed-Tree :
     (y : node-Directed-Tree T) (w : walk-Directed-Tree T y x) →
     walk-fiber-Directed-Tree (y , w) root-fiber-Directed-Tree
-  walk-to-root-fiber-walk-Directed-Tree y refl-walk-Directed-Graph =
-    refl-walk-Directed-Graph
-  walk-to-root-fiber-walk-Directed-Tree .y
-    ( cons-walk-Directed-Graph {y} {z} e w) =
-    cons-walk-Directed-Graph
-      ( e , refl)
-      ( walk-to-root-fiber-walk-Directed-Tree z w)
+  walk-to-root-fiber-walk-Directed-Tree =
+    walk-to-root-fiber-walk-Directed-Graph (graph-Directed-Tree T) x
 
   walk-to-root-fiber-Directed-Tree :
     (y : node-fiber-Directed-Tree) →
     walk-fiber-Directed-Tree y root-fiber-Directed-Tree
-  walk-to-root-fiber-Directed-Tree (y , w) =
-    walk-to-root-fiber-walk-Directed-Tree y w
+  walk-to-root-fiber-Directed-Tree =
+    walk-to-root-fiber-Directed-Graph (graph-Directed-Tree T) x
 ```
 
 ### The fiber of `T` at `x`
 
 ```agda
-  center-unique-parent-fiber-Directed-Tree :
+  center-unique-direct-successor-fiber-Directed-Tree :
     (y : node-fiber-Directed-Tree) →
     ( is-root-fiber-Directed-Tree y) +
     ( Σ ( node-fiber-Directed-Tree) ( edge-fiber-Directed-Tree y))
-  center-unique-parent-fiber-Directed-Tree (y , refl-walk-Directed-Graph) =
-    inl refl
-  center-unique-parent-fiber-Directed-Tree
-    ( y , cons-walk-Directed-Graph {y} {z} e w) = inr ((z , w) , (e , refl))
+  center-unique-direct-successor-fiber-Directed-Tree =
+    center-unique-direct-successor-fiber-Directed-Graph
+      ( graph-Directed-Tree T) x
 
-  contraction-unique-parent-fiber-Directed-Tree :
+  contraction-unique-direct-successor-fiber-Directed-Tree :
     (y : node-fiber-Directed-Tree) →
     ( p :
       ( is-root-fiber-Directed-Tree y) +
       ( Σ ( node-fiber-Directed-Tree) (edge-fiber-Directed-Tree y))) →
-    center-unique-parent-fiber-Directed-Tree y ＝ p
-  contraction-unique-parent-fiber-Directed-Tree ._ (inl refl) = refl
-  contraction-unique-parent-fiber-Directed-Tree
-    ( y , .(cons-walk-Directed-Graph e v)) (inr ((z , v) , e , refl)) =
-    refl
-
-  unique-parent-fiber-Directed-Tree :
-    unique-parent-Directed-Graph
+    center-unique-direct-successor-fiber-Directed-Tree y ＝ p
+  contraction-unique-direct-successor-fiber-Directed-Tree =
+    contraction-unique-direct-successor-fiber-Directed-Graph
+      ( graph-Directed-Tree T) x
+
+  unique-direct-successor-fiber-Directed-Tree :
+    unique-direct-successor-Directed-Graph
       ( graph-fiber-Directed-Tree)
       ( root-fiber-Directed-Tree)
-  pr1 (unique-parent-fiber-Directed-Tree y) =
-    center-unique-parent-fiber-Directed-Tree y
-  pr2 (unique-parent-fiber-Directed-Tree y) =
-    contraction-unique-parent-fiber-Directed-Tree y
+  unique-direct-successor-fiber-Directed-Tree =
+    unique-direct-successor-fiber-Directed-Graph (graph-Directed-Tree T) x
 
   is-tree-fiber-Directed-Tree :
     is-tree-Directed-Graph graph-fiber-Directed-Tree
   is-tree-fiber-Directed-Tree =
-    is-tree-unique-parent-Directed-Graph
-      graph-fiber-Directed-Tree
-      root-fiber-Directed-Tree
-      unique-parent-fiber-Directed-Tree
-      walk-to-root-fiber-Directed-Tree
+    is-tree-fiber-Directed-Graph (graph-Directed-Tree T) x
 
   fiber-Directed-Tree : Directed-Tree (l1 ⊔ l2) (l1 ⊔ l2)
-  pr1 fiber-Directed-Tree = graph-fiber-Directed-Tree
-  pr2 fiber-Directed-Tree = is-tree-fiber-Directed-Tree
+  fiber-Directed-Tree = fiber-Directed-Graph (graph-Directed-Tree T) x
 
-  inclusion-fiber-Directed-Tree :
-    hom-Directed-Tree fiber-Directed-Tree T
-  pr1 inclusion-fiber-Directed-Tree = node-inclusion-fiber-Directed-Tree
-  pr2 inclusion-fiber-Directed-Tree = edge-inclusion-fiber-Directed-Tree
+  inclusion-fiber-Directed-Tree : hom-Directed-Tree fiber-Directed-Tree T
+  inclusion-fiber-Directed-Tree =
+    inclusion-fiber-Directed-Graph (graph-Directed-Tree T) x
 ```
 
 ### Computing the children of a node in a fiber
@@ -176,71 +158,68 @@ module _
   {l1 l2 : Level} (T : Directed-Tree l1 l2) (x : node-Directed-Tree T)
   where
 
-  children-fiber-Directed-Tree :
+  direct-predecessor-fiber-Directed-Tree :
     (y : node-fiber-Directed-Tree T x) → UU (l1 ⊔ l2)
-  children-fiber-Directed-Tree =
-    children-Directed-Tree (fiber-Directed-Tree T x)
+  direct-predecessor-fiber-Directed-Tree =
+    direct-predecessor-fiber-Directed-Graph (graph-Directed-Tree T) x
 
-  children-inclusion-fiber-Directed-Tree :
-    (y : node-fiber-Directed-Tree T x) →
-    children-fiber-Directed-Tree y →
-    children-Directed-Tree T (node-inclusion-fiber-Directed-Tree T x y)
-  children-inclusion-fiber-Directed-Tree =
-    children-hom-Directed-Tree
-      ( fiber-Directed-Tree T x)
-      ( T)
-      ( inclusion-fiber-Directed-Tree T x)
-
-  compute-children-fiber-Directed-Tree :
+  direct-predecessor-inclusion-fiber-Directed-Tree :
     (y : node-fiber-Directed-Tree T x) →
-    children-fiber-Directed-Tree y ≃
-    children-Directed-Tree T (node-inclusion-fiber-Directed-Tree T x y)
-  compute-children-fiber-Directed-Tree y =
-    ( right-unit-law-Σ-is-contr (λ (u , e) → is-contr-total-path' _)) ∘e
-    ( interchange-Σ-Σ _)
+    direct-predecessor-fiber-Directed-Tree y →
+    direct-predecessor-Directed-Tree T
+      ( node-inclusion-fiber-Directed-Tree T x y)
+  direct-predecessor-inclusion-fiber-Directed-Tree =
+    direct-predecessor-inclusion-fiber-Directed-Graph (graph-Directed-Tree T) x
 
-  map-compute-children-fiber-Directed-Tree :
+  compute-direct-predecessor-fiber-Directed-Tree :
     (y : node-fiber-Directed-Tree T x) →
-    children-fiber-Directed-Tree y →
-    children-Directed-Tree T (node-inclusion-fiber-Directed-Tree T x y)
-  map-compute-children-fiber-Directed-Tree y =
-    map-equiv (compute-children-fiber-Directed-Tree y)
+    direct-predecessor-fiber-Directed-Tree y ≃
+    direct-predecessor-Directed-Tree T
+      ( node-inclusion-fiber-Directed-Tree T x y)
+  compute-direct-predecessor-fiber-Directed-Tree =
+    compute-direct-predecessor-fiber-Directed-Graph (graph-Directed-Tree T) x
 
-  htpy-compute-children-fiber-Directed-Tree :
+  map-compute-direct-predecessor-fiber-Directed-Tree :
     (y : node-fiber-Directed-Tree T x) →
-    children-inclusion-fiber-Directed-Tree y ~
-    map-compute-children-fiber-Directed-Tree y
-  htpy-compute-children-fiber-Directed-Tree y t = refl
-
-  inv-compute-children-fiber-Directed-Tree :
+    direct-predecessor-fiber-Directed-Tree y →
+    direct-predecessor-Directed-Tree T
+      ( node-inclusion-fiber-Directed-Tree T x y)
+  map-compute-direct-predecessor-fiber-Directed-Tree =
+    map-compute-direct-predecessor-fiber-Directed-Graph
+      ( graph-Directed-Tree T)
+      ( x)
+
+  htpy-compute-direct-predecessor-fiber-Directed-Tree :
     (y : node-fiber-Directed-Tree T x) →
-    children-Directed-Tree T (node-inclusion-fiber-Directed-Tree T x y) ≃
-    children-fiber-Directed-Tree y
-  inv-compute-children-fiber-Directed-Tree y =
-    inv-equiv (compute-children-fiber-Directed-Tree y)
-
-  Eq-children-fiber-Directed-Tree :
+    direct-predecessor-inclusion-fiber-Directed-Tree y ~
+    map-compute-direct-predecessor-fiber-Directed-Tree y
+  htpy-compute-direct-predecessor-fiber-Directed-Tree =
+    htpy-compute-direct-predecessor-fiber-Directed-Graph
+      ( graph-Directed-Tree T)
+      ( x)
+
+  inv-compute-direct-predecessor-fiber-Directed-Tree :
     (y : node-fiber-Directed-Tree T x) →
-    (u v : children-fiber-Directed-Tree y) → UU (l1 ⊔ l2)
-  Eq-children-fiber-Directed-Tree y u v =
-    Σ ( pr1 (children-inclusion-fiber-Directed-Tree y u) ＝
-        pr1 (children-inclusion-fiber-Directed-Tree y v))
-      ( λ p →
-        tr
-          ( λ t →
-            edge-Directed-Tree T t (node-inclusion-fiber-Directed-Tree T x y))
-          ( p)
-          ( pr2 (children-inclusion-fiber-Directed-Tree y u)) ＝
-            pr2 (children-inclusion-fiber-Directed-Tree y v))
-
-  eq-Eq-children-fiber-Directed-Tree :
+    direct-predecessor-Directed-Tree T
+      ( node-inclusion-fiber-Directed-Tree T x y) ≃
+    direct-predecessor-fiber-Directed-Tree y
+  inv-compute-direct-predecessor-fiber-Directed-Tree =
+    inv-compute-direct-predecessor-fiber-Directed-Graph
+      ( graph-Directed-Tree T)
+      ( x)
+
+  Eq-direct-predecessor-fiber-Directed-Tree :
+    (y : node-fiber-Directed-Tree T x) →
+    (u v : direct-predecessor-fiber-Directed-Tree y) → UU (l1 ⊔ l2)
+  Eq-direct-predecessor-fiber-Directed-Tree =
+    Eq-direct-predecessor-fiber-Directed-Graph (graph-Directed-Tree T) x
+
+  eq-Eq-direct-predecessor-fiber-Directed-Tree :
     (y : node-fiber-Directed-Tree T x) →
-    ( u v : children-fiber-Directed-Tree y) →
-    Eq-children-fiber-Directed-Tree y u v → u ＝ v
-  eq-Eq-children-fiber-Directed-Tree y u v p =
-    map-inv-equiv
-      ( equiv-ap (compute-children-fiber-Directed-Tree y) u v)
-      ( eq-pair-Σ' p)
+    ( u v : direct-predecessor-fiber-Directed-Tree y) →
+    Eq-direct-predecessor-fiber-Directed-Tree y u v → u ＝ v
+  eq-Eq-direct-predecessor-fiber-Directed-Tree =
+    eq-Eq-direct-predecessor-fiber-Directed-Graph (graph-Directed-Tree T) x
 ```
 
 ### The fiber of a tree at a base node
diff --git a/src/trees/fibers-enriched-directed-trees.lagda.md b/src/trees/fibers-enriched-directed-trees.lagda.md
index 09b59777b1..ec2cc9cb37 100644
--- a/src/trees/fibers-enriched-directed-trees.lagda.md
+++ b/src/trees/fibers-enriched-directed-trees.lagda.md
@@ -78,10 +78,12 @@ module _
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( x)
 
-  children-fiber-Enriched-Directed-Tree :
+  direct-predecessor-fiber-Enriched-Directed-Tree :
     (x : node-fiber-Enriched-Directed-Tree) → UU (l3 ⊔ l4)
-  children-fiber-Enriched-Directed-Tree =
-    children-fiber-Directed-Tree (directed-tree-Enriched-Directed-Tree A B T) x
+  direct-predecessor-fiber-Enriched-Directed-Tree =
+    direct-predecessor-fiber-Directed-Tree
+      ( directed-tree-Enriched-Directed-Tree A B T)
+      ( x)
 
   shape-fiber-Enriched-Directed-Tree :
     node-fiber-Enriched-Directed-Tree → A
@@ -92,7 +94,7 @@ module _
   enrichment-fiber-Enriched-Directed-Tree :
     (y : node-fiber-Enriched-Directed-Tree) →
     B (shape-fiber-Enriched-Directed-Tree y) ≃
-    children-fiber-Enriched-Directed-Tree y
+    direct-predecessor-fiber-Enriched-Directed-Tree y
   enrichment-fiber-Enriched-Directed-Tree (y , w) =
     ( interchange-Σ-Σ (λ u e v → v ＝ cons-walk-Directed-Graph e w)) ∘e
     ( ( inv-right-unit-law-Σ-is-contr
@@ -109,7 +111,7 @@ module _
   map-enrichment-fiber-Enriched-Directed-Tree :
     (y : node-fiber-Enriched-Directed-Tree) →
     B ( shape-fiber-Enriched-Directed-Tree y) →
-    children-fiber-Enriched-Directed-Tree y
+    direct-predecessor-fiber-Enriched-Directed-Tree y
   map-enrichment-fiber-Enriched-Directed-Tree =
     map-enrichment-Enriched-Directed-Tree A B fiber-Enriched-Directed-Tree
 
@@ -163,7 +165,7 @@ module _
           ( walk-node-inclusion-fiber-Enriched-Directed-Tree y)))
 ```
 
-### Computing the children of a node in a fiber
+### Computing the direct predecessors of a node in a fiber
 
 ```agda
 module _
@@ -172,50 +174,51 @@ module _
   (x : node-Enriched-Directed-Tree A B T)
   where
 
-  compute-children-fiber-Enriched-Directed-Tree :
+  compute-direct-predecessor-fiber-Enriched-Directed-Tree :
     (y : node-fiber-Enriched-Directed-Tree A B T x) →
-    children-fiber-Enriched-Directed-Tree A B T x y ≃
-    children-Enriched-Directed-Tree A B T
+    direct-predecessor-fiber-Enriched-Directed-Tree A B T x y ≃
+    direct-predecessor-Enriched-Directed-Tree A B T
       ( node-inclusion-fiber-Enriched-Directed-Tree A B T x y)
-  compute-children-fiber-Enriched-Directed-Tree =
-    compute-children-fiber-Directed-Tree
+  compute-direct-predecessor-fiber-Enriched-Directed-Tree =
+    compute-direct-predecessor-fiber-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( x)
 
-  map-compute-children-fiber-Enriched-Directed-Tree :
+  map-compute-direct-predecessor-fiber-Enriched-Directed-Tree :
     (y : node-fiber-Enriched-Directed-Tree A B T x) →
-    children-fiber-Enriched-Directed-Tree A B T x y →
-    children-Enriched-Directed-Tree A B T
+    direct-predecessor-fiber-Enriched-Directed-Tree A B T x y →
+    direct-predecessor-Enriched-Directed-Tree A B T
       ( node-inclusion-fiber-Enriched-Directed-Tree A B T x y)
-  map-compute-children-fiber-Enriched-Directed-Tree =
-    map-compute-children-fiber-Directed-Tree
+  map-compute-direct-predecessor-fiber-Enriched-Directed-Tree =
+    map-compute-direct-predecessor-fiber-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( x)
 
-  inv-compute-children-fiber-Enriched-Directed-Tree :
+  inv-compute-direct-predecessor-fiber-Enriched-Directed-Tree :
     (y : node-fiber-Enriched-Directed-Tree A B T x) →
-    children-Enriched-Directed-Tree A B T
+    direct-predecessor-Enriched-Directed-Tree A B T
       ( node-inclusion-fiber-Enriched-Directed-Tree A B T x y) ≃
-    children-fiber-Enriched-Directed-Tree A B T x y
-  inv-compute-children-fiber-Enriched-Directed-Tree =
-    inv-compute-children-fiber-Directed-Tree
+    direct-predecessor-fiber-Enriched-Directed-Tree A B T x y
+  inv-compute-direct-predecessor-fiber-Enriched-Directed-Tree =
+    inv-compute-direct-predecessor-fiber-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( x)
 
-  Eq-children-fiber-Enriched-Directed-Tree :
+  Eq-direct-predecessor-fiber-Enriched-Directed-Tree :
     (y : node-fiber-Enriched-Directed-Tree A B T x) →
-    (u v : children-fiber-Enriched-Directed-Tree A B T x y) → UU (l3 ⊔ l4)
-  Eq-children-fiber-Enriched-Directed-Tree =
-    Eq-children-fiber-Directed-Tree
+    (u v : direct-predecessor-fiber-Enriched-Directed-Tree A B T x y) →
+    UU (l3 ⊔ l4)
+  Eq-direct-predecessor-fiber-Enriched-Directed-Tree =
+    Eq-direct-predecessor-fiber-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( x)
 
-  eq-Eq-children-fiber-Enriched-Directed-Tree :
+  eq-Eq-direct-predecessor-fiber-Enriched-Directed-Tree :
     (y : node-fiber-Enriched-Directed-Tree A B T x) →
-    ( u v : children-fiber-Enriched-Directed-Tree A B T x y) →
-    Eq-children-fiber-Enriched-Directed-Tree y u v → u ＝ v
-  eq-Eq-children-fiber-Enriched-Directed-Tree =
-    eq-Eq-children-fiber-Directed-Tree
+    ( u v : direct-predecessor-fiber-Enriched-Directed-Tree A B T x y) →
+    Eq-direct-predecessor-fiber-Enriched-Directed-Tree y u v → u ＝ v
+  eq-Eq-direct-predecessor-fiber-Enriched-Directed-Tree =
+    eq-Eq-direct-predecessor-fiber-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( x)
 ```
diff --git a/src/trees/morphisms-directed-trees.lagda.md b/src/trees/morphisms-directed-trees.lagda.md
index b8b59d55da..20aa0fdfc4 100644
--- a/src/trees/morphisms-directed-trees.lagda.md
+++ b/src/trees/morphisms-directed-trees.lagda.md
@@ -66,12 +66,12 @@ module _
       ( graph-Directed-Tree T)
       ( f)
 
-  children-hom-Directed-Tree :
+  direct-predecessor-hom-Directed-Tree :
     (x : node-Directed-Tree S) →
     Σ ( node-Directed-Tree S) (λ y → edge-Directed-Tree S y x) →
     Σ ( node-Directed-Tree T)
       ( λ y → edge-Directed-Tree T y (node-hom-Directed-Tree x))
-  children-hom-Directed-Tree x =
+  direct-predecessor-hom-Directed-Tree x =
     map-Σ
       ( λ y → edge-Directed-Tree T y (node-hom-Directed-Tree x))
       ( node-hom-Directed-Tree)
@@ -182,7 +182,7 @@ module _
       ( f)
       ( g)
 
-  children-htpy-hom-Directed-Tree :
+  direct-predecessor-htpy-hom-Directed-Tree :
     ( α : htpy-hom-Directed-Tree) →
     ( x : node-Directed-Tree S) →
     ( ( tot
@@ -190,9 +190,9 @@ module _
           tr
             ( edge-Directed-Tree T y)
             ( node-htpy-hom-Directed-Tree α x))) ∘
-      ( children-hom-Directed-Tree S T f x)) ~
-    ( children-hom-Directed-Tree S T g x)
-  children-htpy-hom-Directed-Tree α x (y , e) =
+      ( direct-predecessor-hom-Directed-Tree S T f x)) ~
+    ( direct-predecessor-hom-Directed-Tree S T g x)
+  direct-predecessor-htpy-hom-Directed-Tree α x (y , e) =
     eq-pair-Σ
       ( node-htpy-hom-Directed-Tree α y)
       ( ( compute-binary-tr
@@ -284,13 +284,13 @@ module _
       ( is-root-Directed-Tree S x)
       ( Σ (node-Directed-Tree S) (edge-Directed-Tree S x))
       ( λ (y , e) →
-        no-parent-root-Directed-Tree T
+        no-direct-successor-root-Directed-Tree T
           ( tr
             ( λ u → Σ (node-Directed-Tree T) (edge-Directed-Tree T u))
             ( inv H)
             ( node-hom-Directed-Tree S T f y ,
               edge-hom-Directed-Tree S T f e)))
-      ( center (unique-parent-Directed-Tree S x))
+      ( center (unique-direct-successor-Directed-Tree S x))
 
   is-not-root-node-hom-is-not-root-Directed-Tree :
     (x : node-Directed-Tree S) →
diff --git a/src/trees/morphisms-enriched-directed-trees.lagda.md b/src/trees/morphisms-enriched-directed-trees.lagda.md
index e0e1c37f47..adef21dd8f 100644
--- a/src/trees/morphisms-enriched-directed-trees.lagda.md
+++ b/src/trees/morphisms-enriched-directed-trees.lagda.md
@@ -61,7 +61,7 @@ hom-Enriched-Directed-Tree A B S T =
                 ( directed-tree-Enriched-Directed-Tree A B T)
                 ( f)
                 ( x)))
-            ( children-hom-Directed-Tree
+            ( direct-predecessor-hom-Directed-Tree
               ( directed-tree-Enriched-Directed-Tree A B S)
               ( directed-tree-Enriched-Directed-Tree A B T)
               ( f)
@@ -99,7 +99,7 @@ module _
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( directed-tree-hom-Enriched-Directed-Tree)
 
-  children-hom-Enriched-Directed-Tree :
+  direct-predecessor-hom-Enriched-Directed-Tree :
     (x : node-Enriched-Directed-Tree A B S) →
     Σ ( node-Enriched-Directed-Tree A B S)
       ( λ y → edge-Enriched-Directed-Tree A B S y x) →
@@ -107,8 +107,8 @@ module _
       ( λ y →
         edge-Enriched-Directed-Tree A B T y
           ( node-hom-Enriched-Directed-Tree x))
-  children-hom-Enriched-Directed-Tree =
-    children-hom-Directed-Tree
+  direct-predecessor-hom-Enriched-Directed-Tree =
+    direct-predecessor-hom-Directed-Tree
       ( directed-tree-Enriched-Directed-Tree A B S)
       ( directed-tree-Enriched-Directed-Tree A B T)
       ( directed-tree-hom-Enriched-Directed-Tree)
@@ -131,7 +131,7 @@ module _
           ( directed-tree-Enriched-Directed-Tree A B T)
           ( directed-tree-hom-Enriched-Directed-Tree)
           ( x)))
-      ( children-hom-Enriched-Directed-Tree x)
+      ( direct-predecessor-hom-Enriched-Directed-Tree x)
   enrichment-hom-Enriched-Directed-Tree = pr2 (pr2 f)
 ```
 
@@ -190,7 +190,7 @@ module _
                             ( pr1 H x))
                           ( b))) ∙
                       ( ap (λ q → tr B q b) (K x)))))) ~
-            ( ( ( children-htpy-hom-Directed-Tree
+            ( ( ( direct-predecessor-htpy-hom-Directed-Tree
                   ( directed-tree-Enriched-Directed-Tree A B S)
                   ( directed-tree-Enriched-Directed-Tree A B T)
                   ( directed-tree-hom-Enriched-Directed-Tree A B S T f)
diff --git a/src/trees/rooted-morphisms-directed-trees.lagda.md b/src/trees/rooted-morphisms-directed-trees.lagda.md
index 87fdf810c0..dd86d8e2ba 100644
--- a/src/trees/rooted-morphisms-directed-trees.lagda.md
+++ b/src/trees/rooted-morphisms-directed-trees.lagda.md
@@ -91,12 +91,12 @@ module _
     walk-rooted-hom-Directed-Tree =
       walk-hom-Directed-Tree S T hom-rooted-hom-Directed-Tree
 
-    children-rooted-hom-Directed-Tree :
+    direct-predecessor-rooted-hom-Directed-Tree :
       (x : node-Directed-Tree S) →
-      children-Directed-Tree S x →
-      children-Directed-Tree T (node-rooted-hom-Directed-Tree x)
-    children-rooted-hom-Directed-Tree =
-      children-hom-Directed-Tree S T hom-rooted-hom-Directed-Tree
+      direct-predecessor-Directed-Tree S x →
+      direct-predecessor-Directed-Tree T (node-rooted-hom-Directed-Tree x)
+    direct-predecessor-rooted-hom-Directed-Tree =
+      direct-predecessor-hom-Directed-Tree S T hom-rooted-hom-Directed-Tree
 
     preserves-root-rooted-hom-Directed-Tree :
       preserves-root-hom-Directed-Tree hom-rooted-hom-Directed-Tree
@@ -200,17 +200,17 @@ module _
         ( hom-rooted-hom-Directed-Tree S T g)
         ( H)
 
-    children-htpy-rooted-hom-Directed-Tree :
+    direct-predecessor-htpy-rooted-hom-Directed-Tree :
       ( x : node-Directed-Tree S) →
       ( ( tot
           ( λ y →
             tr
               ( edge-Directed-Tree T y)
               ( node-htpy-rooted-hom-Directed-Tree x))) ∘
-        ( children-rooted-hom-Directed-Tree S T f x)) ~
-      ( children-rooted-hom-Directed-Tree S T g x)
-    children-htpy-rooted-hom-Directed-Tree =
-      children-htpy-hom-Directed-Tree S T
+        ( direct-predecessor-rooted-hom-Directed-Tree S T f x)) ~
+      ( direct-predecessor-rooted-hom-Directed-Tree S T g x)
+    direct-predecessor-htpy-rooted-hom-Directed-Tree =
+      direct-predecessor-htpy-hom-Directed-Tree S T
         ( hom-rooted-hom-Directed-Tree S T f)
         ( hom-rooted-hom-Directed-Tree S T g)
         ( H)
diff --git a/src/trees/rooted-morphisms-enriched-directed-trees.lagda.md b/src/trees/rooted-morphisms-enriched-directed-trees.lagda.md
index f3a20c4488..8c97f57574 100644
--- a/src/trees/rooted-morphisms-enriched-directed-trees.lagda.md
+++ b/src/trees/rooted-morphisms-enriched-directed-trees.lagda.md
@@ -90,7 +90,7 @@ module _
       edge-hom-Enriched-Directed-Tree A B S T
         ( hom-rooted-hom-Enriched-Directed-Tree)
 
-    children-rooted-hom-Enriched-Directed-Tree :
+    direct-predecessor-rooted-hom-Enriched-Directed-Tree :
       (x : node-Enriched-Directed-Tree A B S) →
       Σ ( node-Enriched-Directed-Tree A B S)
         ( λ y → edge-Enriched-Directed-Tree A B S y x) →
@@ -98,8 +98,8 @@ module _
         ( λ y →
           edge-Enriched-Directed-Tree A B T y
             ( node-rooted-hom-Enriched-Directed-Tree x))
-    children-rooted-hom-Enriched-Directed-Tree =
-      children-hom-Enriched-Directed-Tree A B S T
+    direct-predecessor-rooted-hom-Enriched-Directed-Tree =
+      direct-predecessor-hom-Enriched-Directed-Tree A B S T
         ( hom-rooted-hom-Enriched-Directed-Tree)
 
     shape-rooted-hom-Enriched-Directed-Tree :
@@ -112,7 +112,7 @@ module _
 
     enrichment-rooted-hom-Enriched-Directed-Tree :
       ( x : node-Enriched-Directed-Tree A B S) →
-      ( ( children-rooted-hom-Enriched-Directed-Tree x) ∘
+      ( ( direct-predecessor-rooted-hom-Enriched-Directed-Tree x) ∘
         ( map-enrichment-Enriched-Directed-Tree A B S x)) ~
       ( ( map-enrichment-Enriched-Directed-Tree A B T
           ( node-rooted-hom-Enriched-Directed-Tree x)) ∘
diff --git a/src/trees/underlying-trees-elements-coalgebras-polynomial-endofunctors.lagda.md b/src/trees/underlying-trees-elements-coalgebras-polynomial-endofunctors.lagda.md
index c72b340ef9..7595d413a1 100644
--- a/src/trees/underlying-trees-elements-coalgebras-polynomial-endofunctors.lagda.md
+++ b/src/trees/underlying-trees-elements-coalgebras-polynomial-endofunctors.lagda.md
@@ -522,7 +522,7 @@ module _
       ( graph-element-coalgebra X w)
       ( root-coalgebra w)
   unique-walk-to-root-element-coalgebra w =
-    is-tree-unique-parent-Directed-Graph'
+    is-tree-unique-direct-successor-Directed-Graph'
       ( graph-element-coalgebra X w)
       ( root-coalgebra w)
       ( has-unique-predecessor-element-coalgebra w)
@@ -917,7 +917,7 @@ module _
   enrichment-compute-enriched-directed-tree-element-coalgebra :
     (x : node-element-coalgebra X w) →
     htpy-equiv
-      ( ( equiv-children-equiv-Directed-Tree
+      ( ( equiv-direct-predecessor-equiv-Directed-Tree
           ( directed-tree-element-coalgebra X w)
           ( combinator-Directed-Tree
             ( λ b →
diff --git a/src/trees/underlying-trees-of-elements-of-w-types.lagda.md b/src/trees/underlying-trees-of-elements-of-w-types.lagda.md
index c417683012..8e259c5013 100644
--- a/src/trees/underlying-trees-of-elements-of-w-types.lagda.md
+++ b/src/trees/underlying-trees-of-elements-of-w-types.lagda.md
@@ -446,7 +446,7 @@ module _
   enrichment-compute-enriched-directed-tree-element-𝕎 :
     (x : node-element-𝕎 w) →
     htpy-equiv
-      ( ( equiv-children-equiv-Directed-Tree
+      ( ( equiv-direct-predecessor-equiv-Directed-Tree
           ( directed-tree-element-𝕎 w)
           ( combinator-Directed-Tree
             ( λ b → directed-tree-element-𝕎 (component-𝕎 w b)))