Enriched directed trees and elements of W-types (#561)

This pull request develops the theory of directed and undirected trees.

- moves polynomial endofunctors and algebras for polynomial endofunctors
to `trees`
- introduces enriched directed trees
- defines some operations on directed trees and enriched directed trees
- defines enriched directed trees for each element of a coalgebra of a
polynomial endofunctor

src/foundation-core/commuting-squares-of-maps.lagda.md

@@ -11,6 +11,7 @@ module foundation-core.commuting-squares-of-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation-core.commuting-triangles-of-maps
 open import foundation-core.functions
 open import foundation-core.homotopies
 open import foundation-core.universe-levels
@@ -46,36 +47,67 @@ coherence-square-maps top left right bottom =
 
 ## Properties
 
-### Composing commuting squares horizontally and vertically
+### Pasting commuting squares horizontally
 
 ```agda
-coherence-square-maps-comp-horizontal :
+module _
   {l1 l2 l3 l4 l5 l6 : Level}
   {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
   (top-left : A → B) (top-right : B → C)
   (left : A → X) (mid : B → Y) (right : C → Z)
-  (bottom-left : X → Y) (bottom-right : Y → Z) →
-  coherence-square-maps top-left left mid bottom-left →
-  coherence-square-maps top-right mid right bottom-right →
-  coherence-square-maps
-    (top-right ∘ top-left) left right (bottom-right ∘ bottom-left)
-coherence-square-maps-comp-horizontal
-  top-left top-right left mid right bottom-left bottom-right sq-left sq-right =
-  (bottom-right ·l sq-left) ∙h (sq-right ·r top-left)
-
-coherence-square-maps-comp-vertical :
+  (bottom-left : X → Y) (bottom-right : Y → Z)
+  where
+
+  pasting-horizontal-coherence-square-maps :
+    coherence-square-maps top-left left mid bottom-left →
+    coherence-square-maps top-right mid right bottom-right →
+    coherence-square-maps
+      (top-right ∘ top-left) left right (bottom-right ∘ bottom-left)
+  pasting-horizontal-coherence-square-maps sq-left sq-right =
+    (bottom-right ·l sq-left) ∙h (sq-right ·r top-left)
+
+  pasting-horizontal-up-to-htpy-coherence-square-maps :
+    {top : A → C} (H : coherence-triangle-maps top top-right top-left)
+    {bottom : X → Z}
+    (K : coherence-triangle-maps bottom bottom-right bottom-left) →
+    coherence-square-maps top-left left mid bottom-left →
+    coherence-square-maps top-right mid right bottom-right →
+    coherence-square-maps top left right bottom
+  pasting-horizontal-up-to-htpy-coherence-square-maps H K sq-left sq-right =
+    ( ( K ·r left) ∙h
+      ( pasting-horizontal-coherence-square-maps sq-left sq-right)) ∙h
+    ( inv-htpy (right ·l H))
+```
+
+### Pasting commuting squares vertically
+
+```agda
+module _
   {l1 l2 l3 l4 l5 l6 : Level}
   {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6}
   (top : A → X)
   (left-top : A → B) (right-top : X → Y)
   (mid : B → Y)
   (left-bottom : B → C) (right-bottom : Y → Z)
-  (bottom : C → Z) →
-  coherence-square-maps top left-top right-top mid →
-  coherence-square-maps mid left-bottom right-bottom bottom →
-  coherence-square-maps
-    top (left-bottom ∘ left-top) (right-bottom ∘ right-top) bottom
-coherence-square-maps-comp-vertical
-  top left-top right-top mid left-bottom right-bottom bottom sq-top sq-bottom =
-  (sq-bottom ·r left-top) ∙h (right-bottom ·l sq-top)
+  (bottom : C → Z)
+  where
+
+  pasting-vertical-coherence-square-maps :
+    coherence-square-maps top left-top right-top mid →
+    coherence-square-maps mid left-bottom right-bottom bottom →
+    coherence-square-maps
+      top (left-bottom ∘ left-top) (right-bottom ∘ right-top) bottom
+  pasting-vertical-coherence-square-maps sq-top sq-bottom =
+    (sq-bottom ·r left-top) ∙h (right-bottom ·l sq-top)
+
+  pasting-vertical-up-to-htpy-coherence-square-maps :
+    {left : A → C} (H : coherence-triangle-maps left left-bottom left-top)
+    {right : X → Z} (K : coherence-triangle-maps right right-bottom right-top) →
+    coherence-square-maps top left-top right-top mid →
+    coherence-square-maps mid left-bottom right-bottom bottom →
+    coherence-square-maps top left right bottom
+  pasting-vertical-up-to-htpy-coherence-square-maps H K sq-top sq-bottom =
+    ( ( bottom ·l H) ∙h
+      ( pasting-vertical-coherence-square-maps sq-top sq-bottom)) ∙h
+    ( inv-htpy (K ·r top))
 ```

src/foundation-core/commuting-triangles-of-maps.lagda.md

@@ -32,6 +32,8 @@ composite map.
 
 ## Definition
 
+### Commuting triangles of maps
+
 ```agda
 module _
   {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
@@ -45,3 +47,19 @@ module _
     (left : A → X) (right : B → X) (top : A → B) → UU (l1 ⊔ l2)
   coherence-triangle-maps' left right top = (right ∘ top) ~ left
 ```
+
+### Concatenation of commuting triangles of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4}
+  (f : A → X) (g : B → X) (h : C → X) (i : A → B) (j : B → C)
+  where
+
+  concat-coherence-triangle-maps :
+    coherence-triangle-maps f g i →
+    coherence-triangle-maps g h j →
+    coherence-triangle-maps f h (j ∘ i)
+  concat-coherence-triangle-maps H K =
+    H ∙h (K ·r i)
+```

src/foundation-core/cones-over-cospans.lagda.md

@@ -174,7 +174,7 @@ module _
   pr2 (pr2 (cone-map c h)) = coherence-square-cone f g c ·r h
 ```
 
-### Horizontal composition of cones
+### Pasting cones horizontally
 
 ```agda
 module _
@@ -183,13 +183,13 @@ module _
   (i : X → Y) (j : Y → Z) (h : C → Z)
   where
 
-  cone-comp-horizontal :
+  pasting-horizontal-cone :
     (c : cone j h B) → cone i (vertical-map-cone j h c) A → cone (j ∘ i) h A
-  pr1 (cone-comp-horizontal c (pair f (pair p H))) = f
-  pr1 (pr2 (cone-comp-horizontal c (pair f (pair p H)))) =
+  pr1 (pasting-horizontal-cone c (pair f (pair p H))) = f
+  pr1 (pr2 (pasting-horizontal-cone c (pair f (pair p H)))) =
     (horizontal-map-cone j h c) ∘ p
-  pr2 (pr2 (cone-comp-horizontal c (pair f (pair p H)))) =
-    coherence-square-maps-comp-horizontal p
+  pr2 (pr2 (pasting-horizontal-cone c (pair f (pair p H)))) =
+    pasting-horizontal-coherence-square-maps p
       ( horizontal-map-cone j h c)
       ( f)
       ( vertical-map-cone j h c)
@@ -209,13 +209,13 @@ module _
   (f : C → Z) (g : Y → Z) (h : X → Y)
   where
 
-  cone-comp-vertical :
+  pasting-vertical-cone :
     (c : cone f g B) → cone (horizontal-map-cone f g c) h A → cone f (g ∘ h) A
-  pr1 (cone-comp-vertical c (pair p' (pair q' H'))) =
+  pr1 (pasting-vertical-cone c (pair p' (pair q' H'))) =
     ( vertical-map-cone f g c) ∘ p'
-  pr1 (pr2 (cone-comp-vertical c (pair p' (pair q' H')))) = q'
-  pr2 (pr2 (cone-comp-vertical c (pair p' (pair q' H')))) =
-    coherence-square-maps-comp-vertical q' p' h
+  pr1 (pr2 (pasting-vertical-cone c (pair p' (pair q' H')))) = q'
+  pr2 (pr2 (pasting-vertical-cone c (pair p' (pair q' H')))) =
+    pasting-vertical-coherence-square-maps q' p' h
       ( horizontal-map-cone f g c)
       ( vertical-map-cone f g c)
       ( g)

src/foundation-core/functoriality-dependent-pair-types.lagda.md

@@ -417,6 +417,17 @@ module _
         ( is-equiv-tot-is-fiberwise-equiv E)
 ```
 
+### `map-Σ` preserves identity maps
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
+  where
+
+  compute-map-Σ-id : map-Σ B id (λ x → id) ~ id
+  compute-map-Σ-id = refl-htpy
+```
+
 ## See also
 
 - Arithmetical laws involving dependent pair types are recorded in

src/foundation-core/functoriality-fibers-of-maps.lagda.md

@@ -49,7 +49,7 @@ map-fib-cone-id g .(g b) (pair b refl) =
 
 ## Properties
 
-### Computing `map-fib-cone` of a horizontal composition of cones
+### Computing `map-fib-cone` of a horizontal pasting of cones
 
 ```agda
 module _
@@ -58,11 +58,11 @@ module _
   (i : X → Y) (j : Y → Z) (h : C → Z)
   where
 
-  map-fib-cone-comp-horizontal :
+  map-fib-pasting-horizontal-cone :
     (c : cone j h B) (d : cone i (pr1 c) A) → (x : X) →
-    ( map-fib-cone (j ∘ i) h (cone-comp-horizontal i j h c d) x) ~
+    ( map-fib-cone (j ∘ i) h (pasting-horizontal-cone i j h c d) x) ~
     ( (map-fib-cone j h c (i x)) ∘ (map-fib-cone i (pr1 c) d x))
-  map-fib-cone-comp-horizontal
+  map-fib-pasting-horizontal-cone
     (pair g (pair q K)) (pair f (pair p H)) .(f a) (pair a refl) =
     eq-pair-Σ
       ( refl)
@@ -76,7 +76,7 @@ module _
               ( inv (ap-concat j (inv (H a)) refl))))))
 ```
 
-### Computing `map-fib-cone` of a horizontal composition of cones
+### Computing `map-fib-cone` of a horizontal pasting of cones
 
 ```agda
 module _
@@ -85,16 +85,16 @@ module _
   (f : C → Z) (g : Y → Z) (h : X → Y)
   where
 
-  map-fib-cone-comp-vertical :
+  map-fib-pasting-vertical-cone :
     (c : cone f g B) (d : cone (pr1 (pr2 c)) h A) (x : C) →
-    ( ( map-fib-cone f (g ∘ h) (cone-comp-vertical f g h c d) x) ∘
+    ( ( map-fib-cone f (g ∘ h) (pasting-vertical-cone f g h c d) x) ∘
       ( inv-map-compute-fib-comp (pr1 c) (pr1 d) x)) ~
     ( ( inv-map-compute-fib-comp g h (f x)) ∘
       ( map-Σ
         ( λ t → fib h (pr1 t))
         ( map-fib-cone f g c x)
         ( λ t → map-fib-cone (pr1 (pr2 c)) h d (pr1 t))))
-  map-fib-cone-comp-vertical
+  map-fib-pasting-vertical-cone
     (pair p (pair q H)) (pair p' (pair q' H')) .(p (p' a))
     (pair (pair .(p' a) refl) (pair a refl)) =
     eq-pair-Σ refl

src/foundation-core/pullbacks.lagda.md

@@ -757,15 +757,15 @@ module _
     is-pullback-rectangle-is-pullback-left-square :
       (c : cone j h B) (d : cone i (vertical-map-cone j h c) A) →
       is-pullback j h c → is-pullback i (vertical-map-cone j h c) d →
-      is-pullback (j ∘ i) h (cone-comp-horizontal i j h c d)
+      is-pullback (j ∘ i) h (pasting-horizontal-cone i j h c d)
     is-pullback-rectangle-is-pullback-left-square c d is-pb-c is-pb-d =
       is-pullback-is-fiberwise-equiv-map-fib-cone (j ∘ i) h
-        ( cone-comp-horizontal i j h c d)
+        ( pasting-horizontal-cone i j h c d)
         ( λ x → is-equiv-comp-htpy
-          ( map-fib-cone (j ∘ i) h (cone-comp-horizontal i j h c d) x)
+          ( map-fib-cone (j ∘ i) h (pasting-horizontal-cone i j h c d) x)
           ( map-fib-cone j h c (i x))
           ( map-fib-cone i (vertical-map-cone j h c) d x)
-          ( map-fib-cone-comp-horizontal i j h c d x)
+          ( map-fib-pasting-horizontal-cone i j h c d x)
           ( is-fiberwise-equiv-map-fib-cone-is-pullback i
             ( vertical-map-cone j h c)
             ( d)
@@ -777,20 +777,20 @@ module _
     is-pullback-left-square-is-pullback-rectangle :
       (c : cone j h B) (d : cone i (vertical-map-cone j h c) A) →
       is-pullback j h c →
-      is-pullback (j ∘ i) h (cone-comp-horizontal i j h c d) →
+      is-pullback (j ∘ i) h (pasting-horizontal-cone i j h c d) →
       is-pullback i (vertical-map-cone j h c) d
     is-pullback-left-square-is-pullback-rectangle c d is-pb-c is-pb-rect =
       is-pullback-is-fiberwise-equiv-map-fib-cone i
         ( vertical-map-cone j h c)
         ( d)
         ( λ x → is-equiv-right-factor-htpy
-          ( map-fib-cone (j ∘ i) h (cone-comp-horizontal i j h c d) x)
+          ( map-fib-cone (j ∘ i) h (pasting-horizontal-cone i j h c d) x)
           ( map-fib-cone j h c (i x))
           ( map-fib-cone i (vertical-map-cone j h c) d x)
-          ( map-fib-cone-comp-horizontal i j h c d x)
+          ( map-fib-pasting-horizontal-cone i j h c d x)
           ( is-fiberwise-equiv-map-fib-cone-is-pullback j h c is-pb-c (i x))
           ( is-fiberwise-equiv-map-fib-cone-is-pullback (j ∘ i) h
-            ( cone-comp-horizontal i j h c d) is-pb-rect x))
+            ( pasting-horizontal-cone i j h c d) is-pb-rect x))
 ```
 
 ### The vertical pullback pasting property
@@ -806,7 +806,7 @@ module _
     is-pullback-top-is-pullback-rectangle :
       (c : cone f g B) (d : cone (horizontal-map-cone f g c) h A) →
       is-pullback f g c →
-      is-pullback f (g ∘ h) (cone-comp-vertical f g h c d) →
+      is-pullback f (g ∘ h) (pasting-vertical-cone f g h c d) →
       is-pullback (horizontal-map-cone f g c) h d
     is-pullback-top-is-pullback-rectangle c d is-pb-c is-pb-dc =
       is-pullback-is-fiberwise-equiv-map-fib-cone
@@ -832,9 +832,9 @@ module _
                 ( λ t → map-fib-cone (horizontal-map-cone f g c) h d (pr1 t)))
               ( map-fib-cone f
                 ( g ∘ h)
-                ( cone-comp-vertical f g h c d)
+                ( pasting-vertical-cone f g h c d)
                 ( vertical-map-cone f g c x))
-              ( map-fib-cone-comp-vertical f g h c d
+              ( map-fib-pasting-vertical-cone f g h c d
                 ( vertical-map-cone f g c x))
               ( is-equiv-inv-map-compute-fib-comp
                 ( vertical-map-cone f g c)
@@ -844,7 +844,7 @@ module _
                 ( f (vertical-map-cone f g c x)))
               ( is-fiberwise-equiv-map-fib-cone-is-pullback f
                 ( g ∘ h)
-                ( cone-comp-vertical f g h c d)
+                ( pasting-vertical-cone f g h c d)
                 ( is-pb-dc)
                 ( vertical-map-cone f g c x)))
             ( pair x refl))
@@ -854,10 +854,10 @@ module _
       (c : cone f g B) (d : cone (horizontal-map-cone f g c) h A) →
       is-pullback f g c →
       is-pullback (horizontal-map-cone f g c) h d →
-      is-pullback f (g ∘ h) (cone-comp-vertical f g h c d)
+      is-pullback f (g ∘ h) (pasting-vertical-cone f g h c d)
     is-pullback-rectangle-is-pullback-top c d is-pb-c is-pb-d =
       is-pullback-is-fiberwise-equiv-map-fib-cone f (g ∘ h)
-        ( cone-comp-vertical f g h c d)
+        ( pasting-vertical-cone f g h c d)
         ( λ x → is-equiv-bottom-is-equiv-top-square
           ( inv-map-compute-fib-comp
             ( vertical-map-cone f g c)
@@ -868,8 +868,8 @@ module _
             ( λ t → fib h (pr1 t))
             ( map-fib-cone f g c x)
             ( λ t → map-fib-cone (horizontal-map-cone f g c) h d (pr1 t)))
-          ( map-fib-cone f (g ∘ h) (cone-comp-vertical f g h c d) x)
-          ( map-fib-cone-comp-vertical f g h c d x)
+          ( map-fib-cone f (g ∘ h) (pasting-vertical-cone f g h c d) x)
+          ( map-fib-pasting-vertical-cone f g h c d x)
           ( is-equiv-inv-map-compute-fib-comp
             ( vertical-map-cone f g c)
             ( vertical-map-cone (horizontal-map-cone f g c) h d)