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.

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 constructing 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.

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:

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.

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.

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:

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.

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:

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:

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$.

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:

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.

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

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'.

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:

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:

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.

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!

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.

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.

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 Natural 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).

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.

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¹, but it's again justified by the setoid model, with only funext needing to be postulated.

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.

  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.

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:

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:

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:

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:

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:

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:

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}$.

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.² 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$.

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.

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.³

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:

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 homomorphism. And the homo (ahem) part is trivial! It's all refls 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.

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.

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.

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.

  (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?

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

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:

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:

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:

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).