defn: initiality implies induction

src/1Lab/Equiv/Fibrewise.lagda.md

@@ -153,3 +153,12 @@ An equivalence over $e$ induces an equivalence of total spaces:
     over→total : P ≃[ e ] Q → Σ A P ≃ Σ B Q
     over→total e' = Σ-ap e λ a → e' a (e.to a) refl
 ```
+
+<!--
+```agda
+subst-fibrewise
+  : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {B' : A → Type ℓ''} (g : ∀ x → B x → B' x)
+  → {x y : A} (p : x ≡ y) (h : B x) → subst B' p (g x h) ≡ g y (subst B p h)
+subst-fibrewise {B = B} {B'} g {x} p h = J (λ y p → subst B' p (g x h) ≡ g y (subst B p h)) (transport-refl _ ∙ ap (g x) (sym (transport-refl _))) p
+```
+-->

src/1Lab/Reflection/Induction/Examples.agda

@@ -4,7 +4,7 @@ open import 1Lab.Path hiding (J)
 open import 1Lab.Type
 
 open import Data.Set.Truncation hiding (∥-∥₀-elim)
-open import Data.Wellfounded.W hiding (W-elim; P)
+open import Data.Wellfounded.W hiding (W-elim)
 open import Data.Fin.Base hiding (Fin-elim)
 open import Data.Id.Base
 

src/Cat/Diagram/Product/Indexed.lagda.md

@@ -105,7 +105,17 @@ Lift-Indexed-product
   : ∀ {ℓ} ℓ' → {I : Type ℓ} → {F : I → C.Ob}
   → Indexed-product {Idx = Lift ℓ' I} (F ⊙ lower)
   → Indexed-product F
-Lift-Indexed-product _ = Indexed-product-≃ (Lift-≃ e⁻¹)
+Lift-Indexed-product _ {F = F} ip = mk where
+  open Indexed-product
+  open is-indexed-product
+  module i = Indexed-product ip
+
+  mk : Indexed-product F
+  mk .ΠF = i.ΠF
+  mk .π i = i.π (lift i)
+  mk .has-is-ip .tuple x = i.tuple (λ j → x (j .lower))
+  mk .has-is-ip .commute = i.commute
+  mk .has-is-ip .unique p q = i.unique _ (λ i → q (i .lower))
 
 is-indexed-product-is-prop
   : ∀ {ℓ'} {Idx : Type ℓ'}

src/Cat/Instances/Poly.lagda.md

@@ -25,7 +25,7 @@ open Total-hom
 ```
 -->
 
-# Polynomial functors and lenses
+# Polynomial functors and lenses {defines="polynomial-functor"}
 
 The category of _polynomial functors_ is the free coproduct completion
 of $\Sets\op$. Equivalently, it is the [[total category]] of the [family

src/Data/Int/Universal.lagda.md

@@ -55,11 +55,13 @@ unique among functions with these properties.
       → ∀ x → f x ≡ map-out p r x
 ```
 
-By a standard categorical argument, existence and uniqueness together give us an
+By a [standard categorical argument], existence and uniqueness together give us an
 *induction principle* for the integers: to construct a section of a type family
 $P : \bb{Z} \to \ty$, it is enough to give an element of $P(0)$ and a family of
 equivalences $P(n) \simeq P(n + 1)$.
 
+[standard categorical argument]: Data.Wellfounded.W.html#initial-algebras-are-inductive-types
+
 ```agda
   ℤ-η : ∀ z → map-out point rotate z ≡ z
   ℤ-η z = sym (map-out-unique id refl (λ _ → refl) z)

src/Data/Wellfounded/W.lagda.md

@@ -11,7 +11,7 @@ open import Data.Wellfounded.Base
 module Data.Wellfounded.W where
 ```
 
-# W-types
+# W-types {defines="w-type"}
 
 The idea behind $W$ types is much simpler than they might appear at
 first brush, especially because their form is like that one of the "big
@@ -62,16 +62,15 @@ subtree of $x$.
 
 <!--
 ```agda
-module _ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') where
+module induction→initial {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') where
 ```
 -->
 
 We can use $W$ types to illustrate the general fact that inductive types
-correspond to *initial algebras* for certain endofunctors. Here, we are working
-in the "ambient" $\io$-category of types and functions, and we are interested in the
-[polynomial functor] `P`{.Agda}:
+correspond to *initial algebras* for certain endofunctors. Here, we are
+working in the "ambient" $\io$-category of types and functions, and we
+are interested in the [[polynomial functor]] `P`{.Agda}:
 
-[polynomial functor]: Cat.Instances.Poly.html
 
 ```agda
   P : Type (ℓ ⊔ ℓ') → Type (ℓ ⊔ ℓ')
@@ -81,36 +80,47 @@ in the "ambient" $\io$-category of types and functions, and we are interested in
   P₁ f (a , h) = a , f ∘ h
 ```
 
-A $P$-**algebra** (or $W$-**algebra**) is simply a type $C$ with a function $P\,C \to C$.
+A $P$-**algebra** (or $W$-**algebra**) is simply a type $C$ with a
+function $P\,C \to C$.
 
 ```agda
   WAlg : Type _
   WAlg = Σ (Type (ℓ ⊔ ℓ')) λ C → P C → C
 ```
 
-Algebras form a [category], where an **algebra homomorphism** is a function that respects
-the algebra structure.
-
-[category]: Cat.Base.html
+Algebras form a [[category]], where an **algebra homomorphism** is a
+function that respects the algebra structure.
 
 ```agda
   _W→_ : WAlg → WAlg → Type _
   (C , c) W→ (D , d) = Σ (C → D) λ f → f ∘ c ≡ d ∘ P₁ f
 ```
 
-Now the inductive `W`{.Agda} type defined above gives us a canonical $W$-algebra:
+<!--
+```agda
+  idW : ∀ {A} → A W→ A
+  idW .fst = id
+  idW .snd = refl
+
+  _W∘_ : ∀ {A B C} → B W→ C → A W→ B → A W→ C
+  (f W∘ g) .fst x = f .fst (g .fst x)
+  (f W∘ g) .snd = ext λ a b → ap (f .fst) (happly (g .snd) (a , b)) ∙ happly (f .snd) _
+```
+-->
+
+Now the inductive `W`{.Agda} type defined above gives us a canonical
+$W$-algebra:
 
 ```agda
   W-algebra : WAlg
   W-algebra .fst = W A B
   W-algebra .snd (a , f) = sup a f
 ```
 
-The claim is that this algebra is special in that it satisfies a *universal property*:
-it is [initial] in the aforementioned category of $W$-algebras.
-This means that, for any other $W$-algebra $C$, there is exactly one homomorphism $I \to C$.
-
-[initial]: Cat.Diagram.Initial.html
+The claim is that this algebra is special in that it satisfies a
+*universal property*: it is [[initial]] in the aforementioned category of
+$W$-algebras. This means that, for any other $W$-algebra $C$, there is
+exactly one homomorphism $I \to C$.
 
 ```agda
   is-initial-WAlg : WAlg → Type _
@@ -168,3 +178,203 @@ Luckily, this is completely straightforward.
     coherent : Square (λ i → unique i ∘ W-algebra .snd) refl hom (λ i → c ∘ P₁ (unique i))
     coherent = transpose (flip₁ (∙-filler _ _))
 ```
+
+## Initial algebras are inductive types
+
+We will now show the other direction of the correspondence: given an
+initial $W$-algebra, we *recover* the type $W_A B$ *and its induction
+principle*, albeit with a propositional computation rule.
+
+<!--
+```agda
+open induction→initial using (WAlg ; is-initial-WAlg ; W-initial) public
+
+module initial→induction {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') (alg : WAlg A B) (init : is-initial-WAlg A B alg) where
+  open induction→initial A B using (_W→_ ; idW ; _W∘_)
+  module _ where private
+```
+-->
+
+It's easy to invert the construction of `W-algebra`{.Agda} to obtain a
+type `W'`{.Agda} and a candidate "constructor" `sup'`{.Agda}, by
+projecting the corresponding components from the given $W$-algebra.
+
+```agda
+    W' : Type _
+    W' = alg .fst
+
+    sup' : (a : A) (b : B a → W') → W'
+    sup' a b = alg .snd (a , b)
+```
+
+<!--
+```agda
+  open Σ alg renaming (fst to W' ; snd to sup')
+```
+-->
+
+We will now show that `W'` satisfies the induction principle of $W_A B$.
+To that end, suppose we have a predicate $P : W' \to \ty$, the
+*motive* for induction, and a function — the *method* $m$ — showing
+$P(\rm{sup}(a, f))$ given the data of the constructor $a : A$, $f :
+(b : B\, a) \to W'$, and the induction hypotheses $f' : (b : B\, a) \to
+P(f b)$.
+
+```agda
+  module
+    _ (P : W' → Type (ℓ ⊔ ℓ'))
+      (psup : ∀ {a f} (f' : (b : B a) → P (f b)) → P (sup' (a , f)))
+    where
+```
+
+The first part of the construction is observing that $m$ is precisely
+what is needed to equip the *total space* $\Sigma_{x : W'} P(x)$ of the
+motive $P$ with $W$-algebra structure.  Correspondingly, we call this a
+"total algebra" of $P$, and write it $\int P$.
+
+```agda
+    total-alg : WAlg A B
+    total-alg .fst = Σ[ x ∈ W' ] P x
+    total-alg .snd (x , ff') = sup' (x , fst ∘ ff') , psup (snd ∘ ff')
+```
+
+By our assumed initiality of $W'$, we then have a $W$-algebra morphism
+$e : W' \to \int P$.
+
+<!--
+```agda
+    private module _ where private
+```
+-->
+
+```agda
+      elim-hom : alg W→ total-alg
+      elim-hom = init total-alg .centre
+```
+
+To better understand this, we can write out the components of this map.
+First, we have an underlying function $W' \to \int P$, which sends an
+element $x : W'$ to a pair $(i, d)$, with $i : W'$ and $d : P(i)$. Since
+$i$ indexes a fibre of $P$, we refer to it as the `index`{.Agda} of the
+result; the returned element $d$ is the `datum`{.Agda}.
+
+```agda
+      index : W' → W'
+      index x = elim-hom .fst x .fst
+
+      datum : ∀ x → P (index x)
+      datum x = elim-hom .fst x .snd
+```
+
+<!--
+```agda
+    open is-contr (init total-alg) renaming (centre to elim-hom)
+    module _ (x : W') where
+      open Σ (elim-hom .fst x) renaming (fst to index ; snd to datum) public
+```
+-->
+
+We also have the equation expressing that `elim-hom`{.Agda} is an
+algebra map, which says that `index`{.Agda} and `datum`{.Agda} both
+commute with supremum, where the second identification depends on the
+first.
+
+```agda
+    beta
+      : (a : A) (f : (x : B a) → W')
+      → (index (sup' (a , f)) , datum (sup' (a , f)))
+        ≡ (sup' (a , index ∘ f) , psup (datum ∘ f))
+    beta a f = happly (elim-hom .snd) (a , f)
+```
+
+The datum part of `elim-hom`{.Agda} is *almost* what we want, but it's
+not quite a section of $P$. To get the actual elimination principle,
+we'll have to get rid of the `index`{.Agda} in its type. The insight now
+is that, much like a [[total category]] admits a projection [[functor]]
+to the base, the total *algebra* of $P$ should admit a projection
+*morphism* to the base $W'$.
+
+The composition
+$$
+W' \xto{e} \smallint P \xto{\pi} W'
+$$
+would then be an algebra morphism, inhabiting the contractible type $W'
+\to W'$, which is also inhabited by the identity. But note that the
+function part of this composition is exactly $i$, so we obtain a
+homotopy $\phi : i \is \id$.
+
+```agda
+    φ : ∀ x → index x ≡ x
+    φ = happly (ap fst htpy) module φ where
+      πe : alg W→ alg
+      πe .fst           = index
+      πe .snd i (a , z) = beta a z i .fst
+
+      htpy = is-contr→is-prop (init alg) πe idW
+```
+
+We can then define the eliminator $e' : \forall x, P\, x$ at $w : W'$ by
+transporting $d(w) : P(i\, w)$ along $\phi$. Since we'll want to
+characterise the value of $e'(\rm{sup}\, f)$ using the second component
+of $\beta$, we can not directly define $\phi$ in terms of the
+composition $\pi \circ e$. Instead, we equip $i$ with a bespoke algebra
+structure, where the proof that $i(\rm{sup}\, f) = \rm{sup}\, (i \circ
+f)$ comes from the *first* component of $\beta$.
+
+```agda
+    elim : ∀ x → P x
+    elim w = subst P (φ w) (datum w)
+```
+
+Since the construction of $\phi$ works at the level of algebra
+morphisms, rather than their underlying functions, we obtain a coherence
+$\psi$, fitting in the diagram below.
+
+~~~{.quiver}
+\[\begin{tikzcd}[ampersand replacement=\&]
+  {\rm{sup}\,(i \circ f)} \&\& {i(\rm{sup}\, f)} \\
+  \\
+  \&\& {\rm{sup} f}
+  \arrow["{\beta_{f}\inv}", from=1-1, to=1-3]
+  \arrow[""{name=0, anchor=center, inner sep=0}, "{\ap{\rm{sup}}{(\phi \circ f)}}"', from=1-1, to=3-3]
+  \arrow["{\phi_{\rm{sup}\, f}}", from=1-3, to=3-3]
+  \arrow["\psi"{description}, draw=none, from=1-3, to=0]
+\end{tikzcd}\]
+~~~
+
+To show that $e'$ commutes with $\rm{sup}$, we can then perform a short
+calculation using the second component of $\beta$, the coherence $\psi$,
+and some stock facts about substitution.
+
+```agda
+    β : (a : A) (f : (x : B a) → W') → elim (sup' (a , f)) ≡ psup (elim ∘ f)
+    β a f =
+      let
+        ψ : ∀ a f → sym (ap fst (beta a f)) ∙ φ (sup' (a , f)) ≡ ap sup'' (funext λ i → φ (f i))
+        ψ a z = square→commutes (λ i j → φ.htpy j .snd (~ i) (a , z)) ∙ ∙-idr _
+      in
+        subst P (φ (sup'' f)) ⌜ datum (sup' (a , f)) ⌝                               ≡⟨ ap! (from-pathp⁻ (ap snd (beta a f))) ⟩
+        subst P (φ (sup'' f)) (subst P (sym (ap fst (beta a f))) (psup (datum ∘ f))) ≡⟨ sym (subst-∙ P _ _ _) ∙ ap₂ (subst P) (ψ a f) refl ⟩
+        subst P (ap sup'' (funext λ z → φ (f z))) (psup (datum ∘ f))                 ≡⟨ nat index datum (funext φ) a f ⟩
+        psup (λ z → subst P (φ (f z)) (datum (f z)))                                 ∎
+```
+
+<!--
+```agda
+      where
+      sup'' : ∀ {a} (f : B a → W') → W'
+      sup'' f = sup' (_ , f)
+
+
+      nat-t : (ix : W' → W') (h : ix ≡ id) (dt : ∀ x → P (ix x)) → _
+      nat-t ix h dt =
+        ∀ a (f : B a → W')
+        → subst P (ap sup'' (funext λ z → happly h (f z))) (psup (dt ∘ f))
+        ≡ psup (λ z → subst P (happly h (f z)) (dt (f z)))
+
+      nat : ∀ ix dt h → nat-t ix h dt
+      nat ix dt h = J (λ ix h → ∀ dt → nat-t ix (sym h) dt)
+        (λ dt a f → Regularity.fast! refl)
+        (sym h) dt
+```
+-->

src/HoTT.lagda.md

@@ -532,6 +532,16 @@ _ = W-initial
 
 * Theorem 5.4.7: `W-initial`{.Agda}
 
+### 5.5: Homotopy-inductive types
+
+<!--
+```agda
+_ = initial→induction.elim
+```
+-->
+
+* Theorem 5.5.5: `initial→induction.elim`{.Agda}
+
 ## Chapter 6: Higher inductive types
 
 ### 6.2: Induction principles and dependent paths