From 6fb97c00ee1c6690aac1617199a78368f919136e Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Wed, 17 Apr 2024 10:55:59 +0200
Subject: [PATCH] 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                    |   2 +
 src/trees/binary-w-types.lagda.md     |  65 +++++
 src/trees/hereditary-w-types.lagda.md | 351 ++++++++++++++++++++++++++
 src/trees/indexed-w-types.lagda.md    |  80 +++++-
 4 files changed, 488 insertions(+), 10 deletions(-)
 create mode 100644 src/trees/binary-w-types.lagda.md
 create mode 100644 src/trees/hereditary-w-types.lagda.md

diff --git a/src/trees.lagda.md b/src/trees.lagda.md
index 18ee699617..4da5e8d445 100644
--- a/src/trees.lagda.md
+++ b/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
diff --git a/src/trees/binary-w-types.lagda.md b/src/trees/binary-w-types.lagda.md
new file mode 100644
index 0000000000..6df97c091c
--- /dev/null
+++ b/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-𝕎
+```
diff --git a/src/trees/hereditary-w-types.lagda.md b/src/trees/hereditary-w-types.lagda.md
new file mode 100644
index 0000000000..3e0ff510c9
--- /dev/null
+++ b/src/trees/hereditary-w-types.lagda.md
@@ -0,0 +1,351 @@
+# Hereditary W-types
+
+```agda
+module trees.hereditary-w-types where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.retractions
+open import foundation.sections
+open import foundation.universe-levels
+
+open import trees.binary-w-types
+```
+
+</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 fixing either `X` or `Y`, we obtain two
+[polynomial endofunctors](trees.polynomial-endofunctors.md) given by
+
+```text
+  Y ↦ Σ (a : A), (B a → X) × (C a → Y)
+```
+
+and
+
+```text
+  X ↦ Σ (a : A), (B a → X) × (C a → Y),
+```
+
+respectively. The type `left-𝕎` is obtained by letting the left argument vary
+and fixing the right argument, i.e., it is the inductive type generated by
+
+```text
+  make-left-𝕎 : (a : A) → (B a → left-𝕎) → (C a → Y) → left-𝕎.
+```
+
+Similarly, the type `right-𝕎` is obtained by fixing the left argument and
+varying the right argument, i.e., it is the inductive type generated by
+
+```text
+  make-right-𝕎 : (a : A) → (B a → X) → (C a → right-𝕎) → right-𝕎.
+```
+
+Thus we obtain two operations `left-𝕎` and `right-𝕎`. The left and right
+{{#concept "hereditary W-type" Agda=left-hereditary-𝕎 Agda=right-hereditary-𝕎}}
+are the least fixed points for the operations `left-𝕎` and `right-𝕎`
+respectively. That is, we define `left-hereditary-𝕎` as the inductive type
+generated by
+
+```text
+  make-left-hereditary-𝕎 : left-𝕎 left-hereditary-𝕎 → left-hereditary-𝕎.
+```
+
+and we define `right-hereditary-𝕎` as the inductive type generated by
+
+```text
+  make-right-hereditary-𝕎 : right-𝕎 right-hereditary-𝕎 → right-hereditary-𝕎.
+```
+
+We will construct equivalences
+
+```text
+  left-hereditary-𝕎 ≃ binary-𝕎
+```
+
+and
+
+```text
+  right-hereditary-𝕎 ≃ binary-𝕎,
+```
+
+showing that both the left and right hereditary W-types are equivalent to the
+binary W-type associated to `B` and `C`.
+
+### Motivating example
+
+If we choose `A := Fin 2` and
+
+```text
+  B 0 := empty        C 0 := empty
+  B 1 := unit         C 1 := unit,
+```
+
+then the left W-type `left-𝕎 B C` is equivalent to the inductive type generated
+by
+
+```text
+  nil : left-𝕎
+  snoc : left-𝕎 → Y → left-𝕎,
+```
+
+which is equivalent to the type `list` of [lists](lists.lists.md). The left
+hereditary W-type `left-hereditary-𝕎` is then equivalent to the type of plane
+trees. Furthermore, in this case the binary W-type associated to `B` and `C` is
+equivalent to the inductive type generated by
+
+```text
+  leaf : left-hereditary-𝕎
+  node : left-hereditary-𝕎 → left-hereditary-𝕎 → left-hereditary-𝕎.
+```
+
+Thus we see that the equivalence `left-hereditary-𝕎 ≃ binary-𝕎` is a
+generalization of the well-known equivalence of plane trees and full binary
+plane trees, which is prominent in the study of the
+[Catalan numbers](elementary-number-theory.catalan-numbers.md).
+
+## Definitions
+
+### Left hereditary W-types
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3)
+  where
+
+  data left-𝕎 {l4 : Level} (Y : UU l4) : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) where
+    make-left-𝕎 : (a : A) → (B a → left-𝕎 Y) → (C a → Y) → left-𝕎 Y
+
+  data left-hereditary-𝕎 : UU (l1 ⊔ l2 ⊔ l3) where
+    make-left-hereditary-𝕎 : left-𝕎 left-hereditary-𝕎 → left-hereditary-𝕎
+```
+
+### Right hereditary W-types
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3)
+  where
+
+  data right-𝕎 {l4 : Level} (X : UU l4) : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) where
+    make-right-𝕎 : (a : A) → (B a → X) → (C a → right-𝕎 X) → right-𝕎 X
+
+  data right-hereditary-𝕎 : UU (l1 ⊔ l2 ⊔ l3) where
+    make-right-hereditary-𝕎 : right-𝕎 right-hereditary-𝕎 → right-hereditary-𝕎
+```
+
+## Properties
+
+### The left hereditary W-type is a fixed point for `left-𝕎`
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3)
+  where
+
+  unpack-left-hereditary-𝕎 :
+    left-hereditary-𝕎 B C → left-𝕎 B C (left-hereditary-𝕎 B C)
+  unpack-left-hereditary-𝕎 (make-left-hereditary-𝕎 T) = T
+
+  is-section-unpack-left-hereditary-𝕎 :
+    is-section make-left-hereditary-𝕎 unpack-left-hereditary-𝕎
+  is-section-unpack-left-hereditary-𝕎 (make-left-hereditary-𝕎 T) = refl
+
+  is-retraction-unpack-left-hereditary-𝕎 :
+    is-retraction make-left-hereditary-𝕎 unpack-left-hereditary-𝕎
+  is-retraction-unpack-left-hereditary-𝕎 T = refl
+
+  is-equiv-make-left-hereditary-𝕎 :
+    is-equiv make-left-hereditary-𝕎
+  is-equiv-make-left-hereditary-𝕎 =
+    is-equiv-is-invertible
+      ( unpack-left-hereditary-𝕎)
+      ( is-section-unpack-left-hereditary-𝕎)
+      ( is-retraction-unpack-left-hereditary-𝕎)
+
+  equiv-make-left-hereditary-𝕎 :
+    left-𝕎 B C (left-hereditary-𝕎 B C) ≃ left-hereditary-𝕎 B C
+  pr1 equiv-make-left-hereditary-𝕎 = make-left-hereditary-𝕎
+  pr2 equiv-make-left-hereditary-𝕎 = is-equiv-make-left-hereditary-𝕎
+```
+
+### The right hereditary W-type is a fixed point for `right-𝕎`
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3)
+  where
+
+  unpack-right-hereditary-𝕎 :
+    right-hereditary-𝕎 B C → right-𝕎 B C (right-hereditary-𝕎 B C)
+  unpack-right-hereditary-𝕎 (make-right-hereditary-𝕎 T) = T
+
+  is-section-unpack-right-hereditary-𝕎 :
+    is-section make-right-hereditary-𝕎 unpack-right-hereditary-𝕎
+  is-section-unpack-right-hereditary-𝕎 (make-right-hereditary-𝕎 T) = refl
+
+  is-retraction-unpack-right-hereditary-𝕎 :
+    is-retraction make-right-hereditary-𝕎 unpack-right-hereditary-𝕎
+  is-retraction-unpack-right-hereditary-𝕎 T = refl
+
+  is-equiv-make-right-hereditary-𝕎 :
+    is-equiv make-right-hereditary-𝕎
+  is-equiv-make-right-hereditary-𝕎 =
+    is-equiv-is-invertible
+      ( unpack-right-hereditary-𝕎)
+      ( is-section-unpack-right-hereditary-𝕎)
+      ( is-retraction-unpack-right-hereditary-𝕎)
+
+  equiv-make-right-hereditary-𝕎 :
+    right-𝕎 B C (right-hereditary-𝕎 B C) ≃ right-hereditary-𝕎 B C
+  pr1 equiv-make-right-hereditary-𝕎 = make-right-hereditary-𝕎
+  pr2 equiv-make-right-hereditary-𝕎 = is-equiv-make-right-hereditary-𝕎
+```
+
+### Left hereditary W-types are binary W-types
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3)
+  where
+
+  binary-left-hereditary-𝕎 : left-hereditary-𝕎 B C → binary-𝕎 B C
+  binary-left-hereditary-𝕎 (make-left-hereditary-𝕎 (make-left-𝕎 a S T)) =
+    make-binary-𝕎 a
+      ( λ b → binary-left-hereditary-𝕎 (make-left-hereditary-𝕎 (S b)))
+      ( λ c → binary-left-hereditary-𝕎 (T c))
+
+  left-hereditary-binary-𝕎 : binary-𝕎 B C → left-hereditary-𝕎 B C
+  left-hereditary-binary-𝕎 (make-binary-𝕎 a S T) =
+    make-left-hereditary-𝕎
+      ( make-left-𝕎 a
+        ( λ b →
+          unpack-left-hereditary-𝕎 B C (left-hereditary-binary-𝕎 (S b)))
+        ( λ c → left-hereditary-binary-𝕎 (T c)))
+
+  is-section-left-hereditary-binary-𝕎 :
+    is-section binary-left-hereditary-𝕎 left-hereditary-binary-𝕎
+  is-section-left-hereditary-binary-𝕎 (make-binary-𝕎 a S T) =
+    ap-binary
+      ( make-binary-𝕎 a)
+      ( eq-htpy
+        ( λ b →
+          ( ap
+            ( binary-left-hereditary-𝕎)
+            ( is-section-unpack-left-hereditary-𝕎 B C
+              ( left-hereditary-binary-𝕎 (S b)))) ∙
+          ( is-section-left-hereditary-binary-𝕎 (S b))))
+      ( eq-htpy (λ c → is-section-left-hereditary-binary-𝕎 (T c)))
+
+  is-retraction-left-hereditary-binary-𝕎 :
+    is-retraction binary-left-hereditary-𝕎 left-hereditary-binary-𝕎
+  is-retraction-left-hereditary-binary-𝕎
+    ( make-left-hereditary-𝕎 (make-left-𝕎 a S T)) =
+    ap
+      ( make-left-hereditary-𝕎)
+      ( ap-binary
+        ( make-left-𝕎 a)
+        ( eq-htpy
+          ( λ b →
+            ap
+              ( unpack-left-hereditary-𝕎 B C)
+              ( is-retraction-left-hereditary-binary-𝕎
+                ( make-left-hereditary-𝕎 (S b)))))
+        ( eq-htpy (λ c → is-retraction-left-hereditary-binary-𝕎 (T c))))
+
+  is-equiv-binary-left-hereditary-𝕎 :
+    is-equiv binary-left-hereditary-𝕎
+  is-equiv-binary-left-hereditary-𝕎 =
+    is-equiv-is-invertible
+      ( left-hereditary-binary-𝕎)
+      ( is-section-left-hereditary-binary-𝕎)
+      ( is-retraction-left-hereditary-binary-𝕎)
+
+  equiv-binary-left-hereditary-𝕎 :
+    left-hereditary-𝕎 B C ≃ binary-𝕎 B C
+  pr1 equiv-binary-left-hereditary-𝕎 = binary-left-hereditary-𝕎
+  pr2 equiv-binary-left-hereditary-𝕎 = is-equiv-binary-left-hereditary-𝕎
+```
+
+### Right hereditary W-types are binary W-types
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3)
+  where
+
+  binary-right-hereditary-𝕎 : right-hereditary-𝕎 B C → binary-𝕎 B C
+  binary-right-hereditary-𝕎 (make-right-hereditary-𝕎 (make-right-𝕎 a S T)) =
+    make-binary-𝕎 a
+      ( λ b → binary-right-hereditary-𝕎 (S b))
+      ( λ c → binary-right-hereditary-𝕎 (make-right-hereditary-𝕎 (T c)))
+
+  right-hereditary-binary-𝕎 : binary-𝕎 B C → right-hereditary-𝕎 B C
+  right-hereditary-binary-𝕎 (make-binary-𝕎 a S T) =
+    make-right-hereditary-𝕎
+      ( make-right-𝕎 a
+        ( λ b → right-hereditary-binary-𝕎 (S b))
+        ( λ c →
+          unpack-right-hereditary-𝕎 B C (right-hereditary-binary-𝕎 (T c))))
+
+  is-section-right-hereditary-binary-𝕎 :
+    is-section binary-right-hereditary-𝕎 right-hereditary-binary-𝕎
+  is-section-right-hereditary-binary-𝕎 (make-binary-𝕎 a S T) =
+    ap-binary
+      ( make-binary-𝕎 a)
+      ( eq-htpy (λ b → is-section-right-hereditary-binary-𝕎 (S b)))
+      ( eq-htpy
+        ( λ c →
+          ( ap
+            ( binary-right-hereditary-𝕎)
+            ( is-section-unpack-right-hereditary-𝕎 B C
+              ( right-hereditary-binary-𝕎 (T c)))) ∙
+          ( is-section-right-hereditary-binary-𝕎 (T c))))
+
+  is-retraction-right-hereditary-binary-𝕎 :
+    is-retraction binary-right-hereditary-𝕎 right-hereditary-binary-𝕎
+  is-retraction-right-hereditary-binary-𝕎
+    ( make-right-hereditary-𝕎 (make-right-𝕎 a S T)) =
+    ap
+      ( make-right-hereditary-𝕎)
+      ( ap-binary
+        ( make-right-𝕎 a)
+        ( eq-htpy (λ b → is-retraction-right-hereditary-binary-𝕎 (S b)))
+        ( eq-htpy
+          ( λ c →
+            ap
+              ( unpack-right-hereditary-𝕎 B C)
+              ( is-retraction-right-hereditary-binary-𝕎
+                ( make-right-hereditary-𝕎 (T c))))))
+
+  is-equiv-binary-right-hereditary-𝕎 :
+    is-equiv binary-right-hereditary-𝕎
+  is-equiv-binary-right-hereditary-𝕎 =
+    is-equiv-is-invertible
+      ( right-hereditary-binary-𝕎)
+      ( is-section-right-hereditary-binary-𝕎)
+      ( is-retraction-right-hereditary-binary-𝕎)
+
+  equiv-binary-right-hereditary-𝕎 :
+    right-hereditary-𝕎 B C ≃ binary-𝕎 B C
+  pr1 equiv-binary-right-hereditary-𝕎 = binary-right-hereditary-𝕎
+  pr2 equiv-binary-right-hereditary-𝕎 = is-equiv-binary-right-hereditary-𝕎
+```
diff --git a/src/trees/indexed-w-types.lagda.md b/src/trees/indexed-w-types.lagda.md
index 7ac1f06423..e8e18992df 100644
--- a/src/trees/indexed-w-types.lagda.md
+++ b/src/trees/indexed-w-types.lagda.md
@@ -14,21 +14,81 @@ open import foundation.universe-levels
 
 ## Idea
 
-**Indexed W-types** are a generalization of ordinary W-types using indexed
-containers. The main idea is that indexed W-types are initial algebras for the
-polynomial endofunctor
+The concept of _indexed W-types_ is a generalization of ordinary
+[W-types](trees.w-types.md) using a dependently typed variant of
+[polynomial endofunctors](trees.polynomial-endofunctors.md). The main idea is
+that indexed W-types are initial
+[algebras](trees.algebras-polynomial-endofunctors.md) for the polynomial
+endofunctor
 
 ```text
-  (X : I → UU) ↦ Σ (a : A i), Π (b : B i a), X (f i a b),
+  (X : I → UU) ↦ (λ (j : I) → Σ (a : A j), Π (i : I), B i j a → X i),
 ```
 
-where `f : Π (i : I), Π (a : A i), B i a → I` is a reindexing function.
+where `B : (i j : I) → A j → 𝒰` is a type family. In other words, given the data
+
+```text
+  A : I → 𝒰
+  B : (i j : I) → A j → 𝒰
+```
+
+of an indexed container we obtain for each `j : I` a multivariable polynomial
+
+```text
+  Σ (a : A j), Π (i : I), B i j a → X i
+```
+
+Since the functorial operation
+
+```text
+  (X : I → UU) ↦ (λ (j : I) → Σ (a : A j), Π (i : I), B i j a → X i),
+```
+
+takes an `I`-indexed family of inputs and returns an `I`-indexed family of
+outputs, it is endofunctorial, meaning that it can be iterated and we can
+consider initial algebras for this endofunctor.
+
+We will formally define the {{#concept "indexed W-type" Agda=indexed-𝕎}}
+associated to the data of an indexed container as the inductive type generated
+by
+
+```text
+  tree-indexed-𝕎 :
+    (x : A j) (α : (i : I) (y : B i j x) → indexed-𝕎 i) → indexed-𝕎 j.
+```
+
+**Note.** In the usual definition of indexed container, the type family `B` is
+directly given as a type family over `A`
+
+```text
+  B : (i : I) → A i → 𝒰,
+```
+
+and furthermore there is a reindexing function
+
+```text
+  j : (i : I) (a : A i) → B i a → I.
+```
+
+The pair `(B , j)` of such a type family and a reindexing function is via
+[type duality](foundation.type-duality.md) equivalent to a single type family
+
+```text
+  (j i : I) → A i → 𝒰.
+```
+
+## Definitions
+
+### The indexed W-type associated to an indexed container
 
 ```agda
 data
-  i𝕎
-    {l1 l2 l3 : Level} (I : UU l1) (A : I → UU l2) (B : (i : I) → A i → UU l3)
-    (f : (i : I) (x : A i) → B i x → I) (i : I) :
-    UU (l2 ⊔ l3) where
-  tree-i𝕎 : (x : A i) (α : (y : B i x) → i𝕎 I A B f (f i x y)) → i𝕎 I A B f i
+  indexed-𝕎
+    {l1 l2 l3 : Level} (I : UU l1) (A : I → UU l2)
+    (B : (i j : I) → A j → UU l3) (j : I) :
+    UU (l1 ⊔ l2 ⊔ l3)
+    where
+  tree-indexed-𝕎 :
+    (x : A j) (α : (i : I) (y : B i j x) → indexed-𝕎 I A B i) →
+    indexed-𝕎 I A B j
 ```