Hereditary W-types (#1112)

In this PR I generalized the equivalence constructed in #1110, to
something that I called "hereditary W-types". This PR is independent of
#1110.

src/trees.lagda.md

@@ -12,6 +12,7 @@ module trees where
 open import trees.algebras-polynomial-endofunctors public
 open import trees.bases-directed-trees public
 open import trees.bases-enriched-directed-trees public
+open import trees.binary-w-types public
 open import trees.bounded-multisets public
 open import trees.coalgebra-of-directed-trees public
 open import trees.coalgebra-of-enriched-directed-trees public
@@ -32,6 +33,7 @@ open import trees.full-binary-trees public
 open import trees.functoriality-combinator-directed-trees public
 open import trees.functoriality-fiber-directed-tree public
 open import trees.functoriality-w-types public
+open import trees.hereditary-w-types public
 open import trees.indexed-w-types public
 open import trees.induction-w-types public
 open import trees.inequality-w-types public

src/trees/binary-w-types.lagda.md

@@ -0,0 +1,65 @@
+# Binary W-types
+
+```agda
+module trees.binary-w-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a type `A` and two type families `B` and `C` over `A`. Then we obtain
+the polynomial functor
+
+```text
+  X Y ↦ Σ (a : A), (B a → X) × (C a → Y)
+```
+
+in two variables `X` and `Y`. By diagonalising, we obtain the
+[polynomial endofunctor](trees.polynomial-endofunctors.md)
+
+```text
+  X ↦ Σ (a : A), (B a → X) × (C a → X).
+```
+
+which may be brought to the exact form of a polynomial endofunctor if one wishes
+to do so:
+
+```text
+  X ↦ Σ (a : A), (B a + C a → X).
+```
+
+The {{#concept "binary W-type" Agda=binary-𝕎}} is the W-type `binary-𝕎`
+associated to this polynomial endofunctor. In other words, it is the inductive
+type generated by
+
+```text
+  make-binary-𝕎 : (a : A) → (B a → binary-𝕎) → (C a → binary-𝕎) → binary-𝕎.
+```
+
+The binary W-type is equivalent to the
+[hereditary W-types](trees.hereditary-w-types.md) via an
+[equivalence](foundation.equivalences.md) that generalizes the equivalence of
+plane trees and full binary plane trees, which is a well known equivalence used
+in the study of the
+[Catalan numbers](elementary-number-theory.catalan-numbers.md).
+
+## Definitions
+
+### Binary W-types
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3)
+  where
+
+  data binary-𝕎 : UU (l1 ⊔ l2 ⊔ l3) where
+    make-binary-𝕎 :
+      (a : A) → (B a → binary-𝕎) → (C a → binary-𝕎) → binary-𝕎
+```