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.

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)

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

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,28 +184,35 @@ 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)
     ( (u , f) , cons-walk-Directed-Graph {_} {y'} e' v) =
     ( ap
       ( tot (λ u → cons-walk-Directed-Tree T e))
       ( cons-cases-contraction-walk-to-base-Directed-Tree g w
-        ( (u , f) , tr-walk-eq-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) →

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)
 ```