---
title: On Induction
date: January 15th, 2021
---

<!--
battle plan:
- motivate induction via lists
  - close enough to naturals that we can appeal to people's intuition about those
- a general schema for normal induction (easy enough)
- handwave about induction-induction (some syntax?) and induction-recursion (a universe?)
- handwave quotient & higher induction-induction
-->

[Last time] on this... thing... I update _very occasionally_, I talked about possible choices for representing equality in type theory. Equality is very important, since many properties of programs and mathematical operators are stated as equalities (e.g., in the definition of a group). However, expressing properties is useless if we can't prove them, and this is where inductive types come in.

[Last time]: /posts/reflections-on-equality.html

Inductive types allow users to extend their type theories with new types, generated by _constructors_, which respect an _induction principle_. Constructors are conceptually simple: they provide a way of *construct*ing elements of that type, like the name implies. The induction principle, though, requires a bit more thought.

The only inductive type
-----------------------

Since this is a blog post about type theory, I am required, by law, to start this discussion about inductive types with the most boring one: the set of all natural numbers, $\mathbb{N}$. The set $\mathbb{N}$ (to be read, and written, `Nat`, from now on) is both uninteresting enough that the discussion can focus on the induction aspect, but also non-trivial enough for some complications to arise.

The type `Nat`{.dt} is generated by two constructors, one for `zero`{.dt}, and one for the `suc`{.dt}cessor of another number. We can represent this in Agda as in the code block below. Taken together, the signature for the type former (`Nat : Set`{.agda}) and the signatures of all the constructors make up the complete specification of the inductive type, called (confusingly) a signature. Looking at only these we can figure out its fundamental property—its induction principle.

```agda
data Nat : Set where
  zero : Nat
  suc  : Nat → Nat
```

Before we consider the full induction principle, it's useful to consider a simply-typed restriction, called the _recursor_. Every inductive type has a recursor, but this name makes the most sense when talking about natural numbers, because it operationally models primitive recursion. The recursor for the natural numbers is a (dependent) function with the following parameters:

- A _motive_, the type we elminate into;
- A _method_ for the constructor `zero`, that is, an element of `A`, and
- A _method_ for the constructor `suc`, which is a function from `A → A`.

To put it into code:

```agda
foldNat : (A : Type) → A → (A → A) → Nat → A
```

Furthermore, the recursor has, as anything in type theory, computational behaviour. That is, when applied to all of its arguments, `foldNat` evaluates. This evaluation is recursive, but pay attention to the structure: we only ever apply `foldNat` to values "smaller" (contained in) the data we started with.

```agda
foldNat : (A : Type) → A → (A → A) → Nat → A
foldNat A z s zero = z
foldNat A z s (suc x) = s (foldNat A z s x)
```

To see how one derives the recursor from the signature, we would have to take a detour through category theory. While a complete semantic argument is preferable, for now, some handwaving is in order. To cite my sources: this presentation of algebras was given in [Kaposi 2020], a very well-written paper which you should check out if you want to understand how algebras work for higher inductive types.

[Kaposi 2020]: https://arxiv.org/pdf/1902.00297.pdf

Take a **`Nat`{.dt}-algebra** to be a dependent triple `(C : Set) × C × (C → C)`{.agda}. The type `C` is known as the _carrier_ of the algebra. From this type of algebras we can define a type family of _`Nat`{.dt}-algebra homomorphisms_ between two algebras, which are structure-preserving maps between them. This definition is a bit complicated, so it's in a box:

```agda
Alg : Set₁
Alg = Σ Set₀ λ Nat → Σ Nat λ _ → (Nat → Nat)

Morphism : Alg → Alg → Set
Morphism (N0 , z0 , s0) (N1 , z1 , s1) =
    Σ (N0 → N1) λ NM →
    Σ (NM z0 ≡ z1) λ _ →
    ((n : N0) → NM (s0 n) ≡ s1 (NM n)) 
```

A morphism between algebras $(N_0, z_0, s_0)$ and $(N_1, z_1, s_1)$ consists of a map $N^M : N_0 \to N_1$ between their carriers together with data proving that $N^M$ maps the objects in $N_0$ to the "right" objects in $N_1$.

Suppose for a second that we have a "special" `Nat`{.dt}-algebra, denoted `Nat*`{.dt}. The statement that there exists a recursion principle for the `Nat`{.dt}ural numbers is then a function with the type boxed below.

```agda
recursion : (α : Alg) → Morphism Nat* α
```

To borrow some more terminology from our category theorist friends, it's stating that `Nat*`{.dt} is _weakly initial_ in the category of `Nat`{.dt}-algebras: For every other algebra `α` we have a homomorphism `Nat* → α`. It turns out that, if our type theory has inductive types, we can implement this function! The initial algebra is given by `(Nat, zero, suc)` and the `recursion` principle by the function below:

```agda
Nat* : Alg
Nat* = (Nat, zero, suc)

recursion : (α : Alg) → Morphism Nat* α
recursion (N0 , z0 , s0) = map , refl , λ n → refl where
  map : Nat → N0
  map zero = z0
  map (suc x) = s0 (map x)
```

In particular, to be very needlessly formal, "every inductive type is the _initial algebra_ of some strictly-positive endofunctor." It's no surprise, then, that we can give such an initial algebra for the natural numbers in Agda, a theory with inductive types! The "shape" of this functor depends on the constructors of the inductive type, but the general principle is the same: Data representing the type (the carrier) together with data for every constructor, with the inductive type "replaced" by the carrier.


And then some more
------------------

A trivial inductive type we can discuss is the unit type, or top type:

```agda
data Unit : Set where
  point : Unit
```

Let's speedrun through the definition of `Unit`{.dt}-algebras, `Unit`{.dt}-algebra homomorphisms, and the initial `Unit`{.dt}-algebra. The name `point`{.dt} was picked for the constructor to be indicative of these structures: `Unit`{.dt} is the _initial pointed type_. A pointed type `T` is a type for which we have a point `p : T`—oops, there's our algebra type! It's `(T : Set) × T`.

_Wait, what? Really?_, I hear you ask. You proceed: _An algebra for the `Unit` type is just a pointed type?_ Yup, my dear reader: the only data we need to eliminate from `Unit` is the type we're eliminating into (the carrier `C`) and a value in `C`, that we map our `point` to!

The family of types between unit types can also be specified in Agda, but I'm absolutely sure you can work it out: It's a function $U^M : U_0 \to U_1$ such that $U^M p_0 \equiv p_1$.

```agda
Unit-Alg : Set₁
Unit-Alg = Σ Set λ Unit → Unit

Unit-Morphism : Unit-Alg → Unit-Alg → Set
Unit-Morphism (U0 , p0) (U1 , p1) = Σ (U0 → U1) λ UM → UM p0 ≡ p1
```

Our definition for Unit-recursion is laughable. It's so trivial that I'm going to go a bit further, and instead of proving _weak_ initiality as we did for the naturals, prove _initiality_: There exists a **unique** map from `(Unit, point)` to any other algebra. For this, we need a notion of uniqueness. Contractibility will do: A type is contractible iff it's pointed and, for every other element, there exists an equality between the point and that element. Check out the box:

```agda
isContr : Set → Set
isContr T = Σ T λ center → (other : T) → other ≡ center
```

Or, this is where I _would_ put a nice box together with an Agda-checked proof that `(Unit , point)` is initial... if I had one! Agda does not have a strong enough notion of equality for us to prove this. In particular, Agda out-of-the-box has no _function extensionality_ principle (see my post on equality). However, we _can_ postulate one, and after writing some equality-manipulation functions, write that proof.

<details>
<summary>Equality stuff</summary>

```agda
postulate
  funext : {ℓ ℓ' : _}
           {A : Set ℓ} {B : A → Set ℓ'}
           (f g : (x : A) → B x)
         → ((x : A) → f x ≡ g x) → f ≡ g

subst : {ℓ ℓ' : _}
        {A : Set ℓ} (B : A → Set ℓ')
        {x y : A}
      → x ≡ y → B x → B y
subst B refl x = x

pairPath : {ℓ ℓ' : _}
           {A : Set ℓ}
           {B : A → Set ℓ'}
           {a b : Σ A B}
           (p : (a ₁) ≡ (b ₁))
         → subst B p (a ₂) ≡ (b ₂)
         → a ≡ b
pairPath {_} {_} {A} {B} {(a , b)} {(a' , b')} refl refl = refl

_∘_ : {ℓ : _} {A : Set ℓ} {x y z : A} → y ≡ z → x ≡ y → x ≡ z
refl ∘ refl = refl

UIP : {ℓ : _} {A : Set ℓ} {x y : A} (p q : x ≡ y) → p ≡ q
UIP refl refl = refl
```

</details>

I'll be the first to admit that all this equality stuff, _especially_ the postulate, is a bit gross. However, it's all justifiable: In particular, the setoid model of type theory validates all of MLTT + funext + UIP, so we're in the clear. The `pairPath` function has a very complicated type: it defines the setoid (or groupoid!) structure of the $\sum$-types.

If you can intuit that an equality between `(a, b) ≡ (c, d)` consists of a pair of equalities `(a ≡ c) × (b ≡ d)`, `pairPath` is that, but dependent. Since the second components of the pairs have types depending on the first element, we need to coerce `e` along the path between `x ≡ y` to get an element `subst B p e : B y` that we can compare with `e'`.

```agda
Unit-initiality : (α : Unit-Alg)
                → isContr (Unit-Morphism (Unit , point) α)
Unit-initiality (U0 , p0) = (map , refl) , contract where
  map : Unit → U0
  map point = p0

  contract : (other : Unit-Morphism (Unit , point) (U0 , p0))
           → other ≡ (map , refl)
  contract ( fun , p ) =
    pairPath
      (funext fun map (λ { point → p }))
      (UIP _ _)
```

With funext, we can also prove `Nat-initiality`, the equivalent statement about natural numbers. Left as an exercise to the reader, though!

Upgrading your recursion: displayed algebras
--------------------------------------------

Just like we can go from regular pairs to dependent pairs by complicating things, we can complicate the recursor to get an _induction principle_, which uniquely characterises each inductive type. From an algebra (the input to the recursor), we build a **displayed algebra**, which is a logical predicate over the algebra's carrier together with proofs for each of its methods. Let's go back to the natural numbers for a second, since those are more interesting than the unit type.

Given a $\mathbb{N}$-algebra $\alpha = (N, z, s)$, we define the type of displayed $\mathbb{N}$-algebras over $\alpha$ to be $\sum(N^D : N \to \mathrm{Set}) \sum(z^D : N^D z) (\prod(n : N) N^D n \to N^D (s\ n))$. That is, we "upgrade" the carrier $N$ to a predicate on carriers $N \to \mathrm{Set}$, $z$ gets upgraded to a proof of $N^D z$, and $s$ gets upgraded to a proof that $N^D (s\ n)$ follows from $N^D n$. Check out the box:

```agda
Nat-Displayed : (α : Nat-Alg) → Set₁
Nat-Displayed (N , z , s) =
  Σ (N → Set) λ Nd →
  Σ (Nd z) λ _ ->
    (n : N) → Nd n → Nd (s n)
```

Now we can finally connect the idea of "inductive types" back to the idea of "induction" that some of us got familiar with in a high school proofs class, namely over the natural numbers:

> Suppose we have a property of the natural numbers, $P$. If:
>
> - $P$ holds for $0$, and
> - Assuming P holds for n, P holds for $n + 1$, then
>
> $P$ holds for every natural number.

This is the same thing we have encoded in the displayed algebras over $(N, z, s)$! Since a predicate is, type-theoretically, a family of types, we interpret our $P$ as $N^D : N \to \mathrm{Set}$. A predicate holds for a value iff you have an inhabitant of the predicate applied to that value, so our proofs become terms of the right type. The universal quantifier for $n$ becomes a dependent function, and the implication a regular function.

The final piece of our complicated terminology puzzle is the idea of a **section** of a displayed algebra over an algebra, a sentence so utterly convoluted that I wish I had never written it. Just like displayed algebras complicate the idea of algebras, sections complicate algebra homomorphisms. Just like a homomorphism has a map between the algebras' carriers, a section has a dependent map from algebra's carrier to the predicate of the algebra displayed over that one. The dependency structure doesn't make a lot of sense written out, so check out the code:

```agda
Nat-Section : (α : Nat-Alg) → Nat-Displayed α → Set
Nat-Section (N , z , s ) (Nd , zd , sd ) =
  Σ ((n : N) → Nd n) λ Ns →
  Σ (Ns z ≡ zd) λ _ →
  ((n : N) → Ns (s n) ≡ sd n (Ns n))
```

The first component of a section is the induced function generated by the motives packaged together by the displayed algebra $(N^D, z^D, s^D)$. The second two components are _reduction rules_, packaged as propositional equalities! The second component, for instance, specifies that $N^S$ (the function) applied to the $z$ero of our algebra returns the method $z^D$.

The existence of an induction principle is packaged up by saying that any algebra displayed over the initial one has a section. In code, it's a dependent map `Induction : (M : Nat-Displayed Nat*) → Section M`{.agda}. We can implement that in Agda like in the box below, but because the `map` obeys the computation rules automatically, none of the proof components are incredibly interesting—they're both trivial proofs.

```agda
Nat-induction : (M : Nat-Displayed Nat*) → Nat-Section Nat* M
Nat-induction (Nd , zd , sd) = map , refl , λ s → refl where
  map : (n : Nat) → Nd n
  map zero = zd
  map (suc x) = sd x (map x)
```

As an _incredibly_ convoluted example we can use all our algebra machinery to implement.. drumroll, please... addition!

```agda
add : Nat → Nat → Nat
add = (Nat-induction displayed) ₁ where
  displayed : Nat-Displayed Nat*
  displayed = (λ n → Nat → Nat)
            , (λ z → z)
            , λ _ k z → suc (k z) 

_ : add (suc (suc zero)) (suc (suc zero))
  ≡ suc (suc (suc (suc zero)))
_ = refl
```

Again using our trivial example as a bit more practice before we move on, let's talk displayed algebras and sections for the Unit type. They're both quite easy. Assuming $(U, p)$ is our algebra, the displayed algebra ends up with a predicate $U^D : U → \mathrm{Set}$ together with a proof $p^D : U\ p$. Sections are also quite easy, since there's only one "propositional reduction rule" to give.

```agda
Unit-Displayed : Unit-Alg → Set₁
Unit-Displayed (U , p) = Σ (U → Set) λ UD → UD p

Unit-Section : (α : Unit-Alg) → Unit-Displayed α → Set
Unit-Section (U , p) (UD , pD) =
  Σ ((x : U) → UD x) λ US →
    US p ≡ pD
```

Agda once more makes the proofs for writing `Unit-Induction` trivial, so I'll leave both its type and implementation as an exercise for the reader.

You saw it coming: Vectors
--------------------------

Both of the exceedingly interesting types we looked at above were simple, since they both just exist in a universe, `Set₀`. Now we up the difficulty considerably by adding both _parameters_ and _indices_. Both are arguments to the type itself, but they differ in how they can be used in the constructors. Again, since I am writing about dependent types, I'm obligated by law to mention this example.. fixed-length lists, or vectors. These are _parametrised_ by a type $A$ of elements and _indexed_ by a number $n : \mathbb{N}$, the length.

```agda
data Vec (A : Set₀) : Nat → Set₀ where
  nil  : Vec A zero
  cons : (n : Nat) → A → Vec A n → Vec A (suc n)
```

Parameters, at least in Agda, are introduced before the `:` in the type signature. Indices come later, but both can be dependent. Parameters have to be the same for every constructor (we only ever mention `Vec A`), but the `Nat`ural can vary between the constructors. One introduces a vector of length zero, and one increments the length of a smaller vector.

The type of algebras for vectors is a tad more interesting, so let's take a look. Since `Vec` is parametrised by `A`, so is `Vec-Alg`. We don't speak of general "vector algebras", only "vector-of-A algebras", so to speak. Since the natural number is an index, it becomes an argument to our carrier type. Both of the "constructor" data are applied to their indices, and since the `A` is bound as an argument to the algebra function, we can refer to it in the type of `cons` (the third component).

```agda
Vec-Alg : Set₀ → Set₁
Vec-Alg A =
  Σ (Nat → Set₀) λ Vec →
  Σ (Vec zero) λ nil →
  {- cons : -} (n : Nat) → A → Vec n → Vec (suc n)
```

The type of homomorphisms for `Vec A`-algebras is mechanically derived from the type above by starting from a map `(n : Nat) → V0 n → V1 n` (where `V0`, `V1` are the carriers of the "source" and "target" algebras) and imposing the necessary conditions.

```agda
Vec-Morphism : (A : Set₀) → Vec-Alg A → Vec-Alg A → Set₀
Vec-Morphism A (V0 , n0 , c0) (V1 , n1 , c1) =
  Σ ((n : Nat) → V0 n → V1 n) λ VM →
  Σ (VM zero n0 ≡ n1) λ _ →
  ((n : Nat) (a : A) (xs : V0 n)
    → VM (suc n) (c0 n a xs) ≡ c1 n a (VM n xs))
```

Just like in the Nat-algebra morphisms, we have two cases, one of which requires exchanging our map with a constructor—the successor/cons case. It's mostly the same, except for the `A` parameter we have to thread everywhere, and all the indices we have to respect. And, just like back then, assuming funext, we have an initial `Vec A`-algebra given by `(Vec A, nil, cons)`. The proof is full of fiddly details[^1], but it's again justified by the setoid model, with only `funext` needing to be postulated.

```agda
Vec-initiality : (A : Set) (α : Vec-Alg A)
               → isContr (Vec-Morphism A (Vec A , nil , cons) α)
Vec-initiality A (V0 , n0 , c0) = (map , resp) , contract where
  map : (n : Nat) → Vec A n → V0 n
  map zero nil = n0
  map (suc n) (cons .n a xs) = c0 n a (map n xs)

  resp = refl , λ n a x → refl
```

Above we provide the map from `Vec A n` to the algebra `α`'s carrier, `V0`, and prove that it `resp`{.kw}ects the equalities imposed by `Vec A`-homomorphisms. Since Agda has pattern matching built in, these equalities are trivial (`refl`{.agda}). Our proof continues upside-down: The interesting thing here is the `map'≡map` equality. Skip the noise: keep reading after the code.

```{.agda .continues}
  contract : (other : Vec-Morphism A (Vec A , nil , cons)
                                     (V0 , n0 , c0))
           → other ≡ (map , refl , λ n a xs → refl)
  contract (map' , nM , cM)
    = pairPath
        map'≡map
        (pairPath
          (UIP _ _)
          (funext3 _ _ (λ n a xs → UIP _ _))) 
    where
      map'~map : (n : Nat) (xs : Vec A n) → map' n xs ≡ map n xs
      map'~map .zero nil = nM
      map'~map .(suc n) (cons n x xs) =
        subst
          (λ e → map' (suc n) (cons n x xs) ≡ c0 n x e)
          (map'~map n xs)
          (cM n x xs)

      map'≡map = funext2 _ _ map'~map
```

We build the `map'≡map`{.va} equality by an appeal to `funext2`{.va}, a helper defined in terms of our `funext`{.op} postulate to reduce the noise a tad. Again, I want to stress that this is a failure of Agda: There is a family of semantic models of type theory in which equality in function types is pointwise _by definition_, including the setoid model, which would be very convenient here since we could keep our appeals to `UIP`{.op}. Anything that validates `funext`{.op} would do, though, including Cubical Agda.

Other than that, the proof is standard: Everything we need is given by the `nM`{.va} and `cM`{.va} equalities of the `other`{.va} morphism we're contracting. In the inductive step, the case for `(cons n x xs)`, we have a path `cM n x xs : map' (suc n) (cons n x xs) ≡ c0 n x (map' n xs)`. Since we want the `map' n xs` on the right-hand side to be `map n xs`, we `subst`{.op} it away using the path `map'~map n xs : map' n xs ≡ map n xs` obtained by a recursive application of `map'~map`{.fn}.

Now we turn to dependent elimination of vectors, or induction. For this we need to calculate the type of displayed algebras over a given `Vec A`-algebra. It's mechanical: The `V` of our algebra gets upgraded to a family of predicates `P : (n : Nat) → V n → Set₀`. The "constructor data" given by `n , c` become "proof data" of a type extending the `Vec A`-algebra.

```agda
Vec-Displayed : (A : Set₀) → Vec-Alg A → Set₁
Vec-Displayed A (V , z , c) =
  Σ ((n : Nat) → V n → Set₀) λ P →
  Σ (P zero z) λ nil →
  {- cons -} (n : Nat) (x : A) (tail : V n)
           → P n tail → P (suc n) (c n x tail)
```

In the `cons` case, the algebra has access both to the `tail` of type `V n` _and_ the inductive assumption `P n tail`. This represents, operationally, a choice between recurring or not.

You know the drill by now: after displayed algebras, algebra sections. Assume an algebra `α = (V, nil, cons)` and a displayed algebra `(P, nD, cD)` over `α`. The first component will be a dependent function of type `(n : Nat) (x : V n) → P n x`, and the second and third components will be propositional equalities representing reduction rules. Since the vectors and natural numbers are similar in structure, we'll end up with similar-looking reduction rules, just noisier. Here they are:

```agda
Vec-Section : (A : Set₀) (α : Vec-Alg A) → Vec-Displayed A α → Set
Vec-Section A (V , n , c) (P , nD , cD) =
  Σ ((n : Nat) (x : V n) → P n x) λ map →
  Σ (map zero n ≡ nD) λ _ →
  ( (n : Nat) (x : A) (tl : V n)
  → map (suc n) (c n x tl) ≡ cD n x tl (map n tl))
```

They're not pretty, so take a minute to internalise them. Again, we have the dependent `map`{.op}, together with a propositional equality which says `map zero n` evaluates to the `nD` datum of our displayed map. The third component specifies that `map (suc n)` defers to the `cD` component and recurs in the tail. It's not complicated conceptually, but it is complex to write down. Finally, the induction principle for natural numbers says that any displayed algebra over the initial `(Vec A , nil , cons)` has a section. Again, Agda trivialises the equalities:

```agda
Vec-Induction : (A : Set₀)
                (α : Vec-Displayed A (Vec A , nil , cons))
              → Vec-Section A (Vec A , nil , cons) α
Vec-Induction A (P , nD , cD) = map , refl , λ n a xs → refl where
  map : (n : Nat) (xs : Vec A n) → P n xs
  map .zero nil              = nD
  map .(suc n) (cons n x xs) = cD n x xs (map n xs)
```

I bet you've never seen types like these
----------------------------------------

This is a bet I'm willing to take. Unless you've gone looking for ways to formalise semantics of inductive types before, it's not very likely for you to have come across this algebra machinery before. A far more common way of dealing with inductive data types is dependent pattern matching:

```agda
add : Nat → Nat → Nat
add zero n    = n
add (suc x) n = suc (x + n)

map : {n : Nat} {A B : Set₀} → (A → B) → Vec A n → Vec B n
map f nil = nil
map f (cons x xs) = cons (f x) (map f xs)
```

However, there is a very good reason not to work directly with pattern matching in a formalisation. That reason can be found on page 24 of [this paper] by Cockx et al. Take a minute to recover and we can continue talking. A more tractable presentation of inductive types is directly with induction principles, instead of taking this detour through category theory. For instance, the natural numbers:

```agda
Nat-induction : (P : Nat → Set)
              → P zero
              → ((n : Nat) → P n → P (suc n))
              → (n : Nat) → P n
Nat-induction P pz ps zero    = pz
Nat-induction P pz ps (suc n) = ps n (Nat-induction P pz ps)
```

It turns out that this presentation, and the one based on algebras I've been going on about, are actually equivalent! Very plainly so. If you unfold the type of `Nat-Induction` (the one about algebras), and do some gratuitous renaming, you get this:

```agda
Nat-Induction :
  (M :     Σ (Nat → Set)
     λ P → Σ (P zero)
     λ _ → (n : Nat) → P n → P (suc n)
  )
  →           Σ ((n : Nat) → M ₁ n)
  λ Nat-ind → Σ (Nat-ind zero ≡ M ₂ ₁)
  λ _       → (n : Nat) → Nat-ind (suc n) = M ₂ ₂ n (Nat-ind n)
```

It's ugly, especially with all the subscript projections, but if we apply some good ol' currying we can recover this type, by transforming (the dependent analogue of) `A × B × C → D` with `A → B → C → D`:

```agda
Nat-Induction : (P     : Nat → Set)
                (pzero : P zero)
                (psuc  : (n : Nat) → P n → P (suc n))
              → Σ ((n : Nat) → P n)
        λ ind → Σ (ind zero ≡ pzero)
        λ _   → (n : Nat) → ind (suc n) ≡ psuc n (ind n)
```

I've gone and done some more renaming. `P` is a name for `M ₁`, `pzero` is `M ₂ ₁`, and `psuc` is `M ₂ ₂`. Again, just to emphasise what the contents of "a displayed algebra section over the initial algebra" turn out to be:

- The first component is **a function from the data type to a predicate**,
- The $n$ following components are **propositional equalities representing reduction rules**, for each constructor, recurring as appropriate.

If you'll allow me one of _those_ asides, this is just incredibly cool to me. The fact we can start from an inductive signature and derive not only the recursor, but from that derive the motives and methods of induction, and from _that_ derive exactly the behaviour of the induced map for a particular bundle of motives and methods? It feels.. right. Like this is what induction was meant to be. Not some needlessly formal underpinning for pattern matching, like I used to think of it as, but as distinguished, rich mathematical objects determined exactly by their constructors.

Complicating it further: Induction-induction
--------------------------------------------

We've seen, in the past 2 thousand-something words, how to build algebras, algebra homomorphisms, displayed algebras and algebra sections for inductive types, both indexed and not. Now, we'll complicate it further: Induction-induction allows the formation of two inductive families of types $A : \mathrm{Set}$ and $B : A \to \mathrm{Set}$ _together_, such that the constructors of A can refer to those of B and vice-versa.

The classic example is defining a type together with an inductively-defined predicate on it, for instance defining sorted lists together with a "less than all elements" predicate in one big induction. However, in the interest of brevity, I'll consider a simpler example: A syntax for contexts and Π-types in type theory. We have one base type, `ι`, which is valid in any context, and a type for dependent products `Π`. Its type expresses the rule for $\prod$-introduction, which says that given $\Gamma \vdash \sigma\ \mathrm{type}$ and $\Gamma, \sigma \vdash \tau\ \mathrm{type}$, then $\Gamma \vdash (\prod(\sigma) \tau)\ \mathrm{type}$.

```agda
data Ctx : Set
data Ty : Ctx → Set

data Ctx where
  stop : Ctx
  pop  : (Γ : Ctx) → Ty Γ → Ctx

data Ty where
  ι  : {Γ : Ctx} → Ty Γ
  Π  : {Γ : Ctx} (σ : Ty Γ) (τ : Ty (pop Γ σ)) → Ty Γ
```

Here I'm using Agda's forward-declaration feature to specify the signatures of `Ctx` and `Ty` before their constructors. This is because the constructors of `Ctx` mention the type `Ty`, and the type _of_ `Ty` mentions `Ctx`, so there's no good way to untangle them.

When talking about our standard set of categorical gizmos for inspecting values of inductive type, it's important to note that, just like we can't untangle the definitions of `Ctx` and `Ty`, we can't untangle their algebras either. Instead of speaking of `Ctx`-algebras or `Ty`-algebras, we can only talk of `Ctx-Ty`-algebras.[^2] Let's think through the algebras first, since the rest are derived from that.

For our `Nat`-algebras, we had as a carrier an element of `Set₀`. For the `Vec`-algebras, we needed a carrier which was an element of `Nat → Set₀`. Now, since we have two types, one of which is indexed, we can't describe their carriers in isolation: We have a _telescope_ of carriers $Σ (\mathrm{Ty}^A : \mathrm{Set}_0) Σ (\mathrm{Ctx}^A : \mathrm{Ty}^A \to \mathrm{Set}_0)$ over which the type of the methods is quantified. Let's go through them in order.

- `stop : Ctx` gives rise to a method $\mathrm{stop}^A : \mathrm{Ctx}^A$,
- `pop  : (Γ : Ctx) → Ty Γ → Ctx` generates a method $\mathrm{pop}^A : (Γ^A : \mathrm{Ctx}^A) → \mathrm{Ty}^A\ Γ^A → \mathrm{Ctx}^A$
- `ι : {Γ : Ctx} → Ty Γ` leads us to jot down a method $\iota^A : \{Γ^A : \mathrm{Ctx}^A\} → \mathrm{Ty}^A\ \Gamma^A$
- `Π : {Γ : Ctx} (σ : Ty Γ) (τ : Ty (pop Γ σ)) → Ty Γ` finally gives us a method with the hell-of-a-type
  $\Pi^A : \{\Gamma^A : \mathrm{Ctx}^A\} (\sigma^A : \mathrm{Ty}^A\ \Gamma) (\tau : \mathrm{Ty}^A (\mathrm{pop}^A\ \Gamma^A\ \sigma^A) → \mathrm{Ty}^A\ \Gamma^A)$

Let's go back to Agda-land, where I will write exactly the same thing but with syntax somehow even less convenient than LaTeX. Just as a reminder, `Σ A λ x → B` is how I've been writing $\sum(x : A) B$.

```agda
Ctx-Ty-Alg : Set₁
Ctx-Ty-Alg =
  Σ Set₀ λ Ctx →
  Σ (Ctx → Set₀) λ Ty →
  Σ Ctx λ stop →
  Σ ((Γ : Ctx) → Ty Γ → Ctx) λ pop →
  Σ ({Γ : Ctx} → Ty Γ) λ ι →
  ({Γ : Ctx} (σ : Ty Γ) (τ : Ty (pop Γ σ)) → Ty Γ)
```

The type of homomorphisms for these algebras are the same as the ones we've seen before, except for the fact they're way more complicated. Both of the carrier components still become functions, and all of the method components still become equalities which must be respected, except now there's more of them.

```{.agda tag=Suffering}
Ctx-Ty-Morphism : Ctx-Ty-Alg → Ctx-Ty-Alg → Set₀
Ctx-Ty-Morphism
  (C0 , T0 , s0 , p0 , i0 , f0)
  (C1 , T1 , s1 , p1 , i1 , f1)
  =
    Σ (C0 → C1) λ Ctx →
    Σ ((x : C0) → T0 x → T1 (Ctx x)) λ Ty →

    -- Constructor data for Ctx
    Σ (Ctx s0 ≡ s1) λ stop →
    Σ ( (x : C0) (ty : T0 x)
      → Ctx (p0 x ty) ≡ p1 (Ctx x) (Ty x ty))
    λ pop →

    -- Constructor data for Ty
    Σ ({Γ : C0} → Ty Γ (i0 {Γ}) ≡ i1 {Ctx Γ}) λ iota →
    ( {Γ : C0} (σ : T0 Γ) (τ : T0 (p0 Γ σ))
    → Ty Γ (f0 {Γ} σ τ)
    ≡ f1 (Ty Γ σ) (subst T1 (pop Γ σ) (Ty (p0 Γ σ) τ)))
```

Ok, I lied. There's more than just the usual "more stuff" complication. In the case for `Π` (nameless, the last component), we need to compare `f0 σ τ` with `f1 (Ty Γ σ) (Ty (p0 Γ σ) τ)`. Read past the symbols: We need to make sure that the `Ty` operation maps `Π` types to `Π` types. But, there's a catch! `Ty (p0 Γ σ) τ)` has type `T1 (Ctx (p0 Γ σ))` (i.e., assemble the context in `C0` with `p0`, then translate to `C1` with `T1`), but `f1` wants something in `T1 (p1 (Ctx Γ) (Ty Γ σ))` (assemble the context in `C1` with translated components).

We know these types are equal though, the equation `pop` says _just that_! Agda isn't that clever, though (thankfully), so we have to manually cast along the path `pop Γ σ` to make these types line up. Since we have so many equations, we definitely would've ended up with at least one dependent path.[^3]

I'll pass on proving strict initiality in the interest of brevity, settling for the weak variant. Recall that initiality means we have a distinguished `Ctx-Ty`-algebra, given by the type formers and constructors, from which we can make a morphism to any other algebra. In types:

```agda
Ctx-Ty-Initial : (M : Ctx-Ty-Alg) → Ctx-Ty-Morphism Ctx-Ty* M
Ctx-Ty-Initial (C0 , T0 , s0 , p0 , i0 , f0)
  = C , T , refl , (λ x ty → refl) , refl , λ σ τ → refl
  where
    C : Ctx → C0
    T : (x : Ctx) → Ty x → T0 (C x)

    C stop = s0
    C (pop c t) = p0 (C c) (T c t)

    T γ ι = i0 {C γ}
    T γ (Π σ τ) = f0 (T γ σ) (T (pop γ σ) τ)
```

I want to make clear that, while this looks like a bloody mess, it was incredibly simple to implement. See the equation `T γ (Π σ τ) = ...`? I didn't write that. I didn't _need_ to. Check out the type of the last component of `Ctx-Ty-Morphism Ctx-Ty* M`. It's literally just saying what the right-hand-side of `T γ (Π σ τ)` needs to be for `(C, T)` to be the morphism part of a **homo**morphism. And the homo (ahem) part is trivial! It's all `refl`s again (are you noticing a trend?).

Elevating it: Higher Inductive Types
------------------------------------

The algebra approach isn't limited to the `Set`-level mathematics we've been doing up to now, and it scales very simply to types with path constructors in addition to point constructors. For this part, we unfortunately can't _implement_ any of the proofs in standard Agda, especially Agda `--with-K` that we've been using up to now, but we can still talk about their types. Let's start with the second simplest higher inductive type: Not the circle, but the interval.

The interval has two endpoints, `l` and `r`, and a line `seg`{.op}ment between them. It's a contractible type, so it's equivalent to the Unit type we've seen before, but it's.. more. The existence of the interval type implies funext, and we'll show that using algebras.

```agda
data I : Type₀ where
  l r : I
  seg : i0 ≡ i1
```

The type of algebras for the interval is also simple. We have a carrier, $I^A$, two points $l^A : I^A$ and $r^A : I^A$, and an _equality_ $seg^A : l^A \equiv r^A$. Wait, an equality? Yup! Since the enpoinds `l` and `r` are equal, so must be whatever they map to. But, since we're in HoTT-land now, this equality doesn't necessarily need to be trivial, as we'll see in a second.

```agda
I-Alg : Type₁
I-Alg = Σ Type₀ λ I → Σ I λ l → Σ I λ r → l ≡ r
```

The type of algebra homomorphisms, like before, encompasses a map together with some propositional reductions of that map. We have three "standard" components `I`, `l`, `r`, which are just like for the type of booleans, and a mystery fourth component which expresses the right coherence condition.

```agda
I-Alg-Morphism : I-Alg → I-Alg → Type
I-Alg-Morphism (I0 , l0 , r0 , seg0) (I1 , l1 , r1 , seg1) = 
  Σ (I0 → I1) λ I →
  Σ (I l0 ≡ l1) λ l →
  Σ (I r0 ≡ r1) λ r →
```

Now the type of the fourth component is interesting. We want `seg0` and `seg1` to be "equal" in some appropriate sense of equality. But they have totally different types! `seg0 : l0 ≡I0 r0` and `seg1 : l1 ≡I1 r1`. It's easy enough to fix the type of `seg0` to be a path in `I1`: Since `I : I0 → I1`, its action on paths `ap I seg0` is a path in `I1` between `I l0` and `I r0`. Out of the pan, into the fire, though. Now the endpoints don't match up!

Can we fix `I l0` and `I r0` in the endpoints of `seg0`? The answer, it turns out, is yes. We can use path _transitivity_ to alter both endpoints. `r` correctly lets us go from `I r0` to `r1`, but `l` is wrong—it takes `l1` to `I r0`. We want that backwards, so we apply _symmetry_ here.

```agda
  (r ∘ (ap I seg0 ∘ sym l)) ≡ seg1
```

Now, I'll reproduce an argument from the HoTT book, which proves function extensionality follows from the interval type and its eliminator. But we'll do it with algebras. First, we need to postulate (since Agda is weak), that there exists a weakly initial `I`-algebra. This'll play the part of our data type. In reality, there's a couple more details, but we can ignore those, right?

<details>
<summary>We can't.</summary>

Instead of just full-on postulating the existence of an `I`-algebra and its initiality, I'll define the type `I` (lacking its `seg`) normally, postulate `seg`, then postulate the coherence condition in the definition of `I-Recursion`. This simplifies some proofs since it means `I-Recursion` will compute definitionally on point constructors.

```agda
data I : Type where
  l r : I

postulate
  seg : l ≡ r

I* : I-Alg
I* = (I , l , r , seg)

I-Recursion : (α : I-Alg) → I-Alg-Morphism I* α
I-Recursion (I0 , l0 , r0 , seg0) = go , refl , refl , subst (λ e → e ≡ seg0) (∘refl (ap go seg)) sorry where
  go : I → I0
  go l = l0
  go r = r0

  postulate
    sorry : ap go seg ≡ seg0
```

There's a bit of ugly equality-wrangling still, but it's fine. All that matters is that it type checks, I suppose.

</details>

Now, the argument. We want a function that, given $f, g : A \to B$ and a homotopy $p : \prod(x : A) \to f(x) \equiv g(x)$, produces a path $f \equiv g$. We define a family of functions $h_x : I \to B$ given a $x : A$, which maps `l` to `f(x)`, `r` to `g(x)`, and in the "`seg` case", returns `p(x)`. The algebra is simple:

```agda
I→funext : {A B : Type} (f g : A → B) (hom : (x : A) → f x ≡ g x) → f ≡ g
I→funext {A} {B} f g p = ? where
  h : A → I → B
  h x = (I-Recursion (B , f x , g x , p x)) ₁
```

And for my next trick, I'll define the function `h' = flip h`. Or, in Agda terms, `h' = λ i x → h x i`, a function from `I → A → B`. We have a path between the two endpoints of the segment, so we also have a path between the two "endpoinds" of this function, which we can calculate:

```{.agda tag="Mmm, substitution"}
ap h' seg : (λ i x → h x i) l ≡ (λ i x → h x i) r -- type of ap
          =     (λ x → h x l) ≡ (λ x → h x r)     -- β-reduce
          =       (λ x → f x) ≡ (λ x → g x)       -- computation for h
          =                 f ≡ g                 -- η-reduce
```

This concludes our proof:

```agda
I→funext : {A B : Type} (f g : A → B) (hom : (x : A) → f x ≡ g x) → f ≡ g
I→funext {A} {B} f g p = ap h' seg where
  h : A → I → B
  h x = (I-Recursion (B , f x , g x , p x)) ₁

  h' : I → A → B
  h' i x = h x i
```

This concludes our post
-----------------------

God, this was a long one. Four thousand words! And a bit more, with this conclusion.

I've wanted to write about inductive types for a hecking long time now, ever since the day I finished the equality post. However, coming by motivations in the past year has been.. hard, for everyone. So it's good that I finally managed to it out there! _77 days later_. God. I might write some more type theory in the future, but don't hold your breath! 77 days is like, 36 thousand times more than you could do that for.

I ended up writing about algebras instead of eliminators or pattern matching because they seamlessly scale up even to higher induction-induction, which ends up having super complicated eliminators, far too much for me to derive by hand (especially early in the AMs, which is when most of this post was written).

<div class="special-thanks">
With special thanks to the proofreader:

* [My friend Jonathan](https://squiddev.cc)
</div>

[this paper]: https://dl.acm.org/doi/10.1145/3236770

[^1]: And, full disclosure, took me almost an hour to write at 2 AM...
[^2]: The best part of this presentation is that it makes painfully clear the infernal way that everything in type theory depends on everything else.
[^3]: Please forgive my HoTT accent.