5.5 Homotopy-inductive types

In §5.3 (http://planetmath.org/53wtypes) we showed how to encode natural numbers as $𝖶$-types, with

${𝐍}^{𝐰}$ $:\equiv {𝖶}_{(b:\mathrm{𝟐})}{\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟐}}(𝒰,\mathrm{𝟎},\mathrm{𝟏}),$

$0^{𝐰}$ $:\equiv \mathrm{𝗌𝗎𝗉}(0_{\mathrm{𝟐}},(\lambda x.{\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟎}}({𝐍}^{𝐰},x))),$

${𝐬}^{𝐰}$ $:\equiv \lambda n.\mathrm{𝗌𝗎𝗉}(1_{\mathrm{𝟐}},(\lambda x.n)).$

We also showed how one can define a $\mathrm{𝖽𝗈𝗎𝖻𝗅𝖾}$ function on ${𝐍}^{𝐰}$ using the recursion principle. When it comes to the induction principle, however, this encoding is no longer satisfactory: given $E:{𝐍}^{𝐰}\to 𝒰$ and recurrences $e_z:E(0^{𝐰})$ and $e_s:{\prod }_{(n:{𝐍}^{𝐰})}{\prod }_{(y:E(n))}E({𝐬}^{𝐰}(n))$, we can only construct a dependent function $r(E,e_z,e_s):{\prod }_{(n:{𝐍}^{𝐰})}E(n)$ satisfying the given recurrences propositionally, i.e. up to a path. This means that the computation rules for natural numbers, which give judgmental equalities, cannot be derived from the rules for $𝖶$-types in any obvious way.

This problem goes away if instead of the conventional inductive types we consider homotopy-inductive types, where all computation rules are stated up to a path, i.e. the symbol $\equiv$ is replaced by $=$. For instance, the computation rule for the homotopy version of $𝖶$-types ${𝖶}^{𝗁}$ becomes:

• For any $a:A$ and $f:B(a)\to {𝖶}_{(x:A)}^{h}B(x)$ we have

  $${\mathrm{𝗋𝖾𝖼}}_{{𝖶}_{(x:A)}^{h}B(x)}(E,\mathrm{𝗌𝗎𝗉}(a,f))=e(a,f,(\lambda b.{\mathrm{𝗋𝖾𝖼}}_{{𝖶}_{(x:A)}^{h}B(x)}(E,f(b))))$$

Homotopy-inductive types have an obvious disadvantage when it comes to computational properties — the behavior of any function constructed using the induction principle can now only be characterized propositionally. But numerous other considerations drive us to consider homotopy-inductive types as well. For instance, while we showed in §5.4 (http://planetmath.org/54inductivetypesareinitialalgebras) that inductive types are homotopy-initial algebras, not every homotopy-initial algebra is an inductive type (i.e. satisfies the corresponding induction principle) — but every homotopy-initial algebra is a homotopy-inductive type. Similarly, we might want to apply the uniqueness argument from §5.2 (http://planetmath.org/52uniquenessofinductivetypes) when one (or both) of the types involved is only a homotopy-inductive type — for instance, to show that the $𝖶$-type encoding of $\mathbb{N}$ is equivalent to the usual $\mathbb{N}$.

Additionally, the notion of a homotopy-inductive type is now internal to the type theory. For example, this means we can form a type of all natural numbers objects and make assertions about it. In the case of $𝖶$-types, we can characterize a homotopy $𝖶$-type ${𝖶}_{(x:A)}B(x)$ as any type endowed with a supremum function and an induction principle satisfying the appropriate (propositional) computation rule:

$$\begin{array}{c}{𝖶}_d(A,B):\equiv \sum _{W:𝒰}\sum _{(\mathrm{𝗌𝗎𝗉}:{\prod }_{(a)}(B(a)\to W)\to W)}\prod _{(E:W\to 𝒰)}\hfill \\ \hfill \prod _{(e:{\prod }_{(a,f)}({\prod }_{(b:B(a))}E(f(b)))\to E(\mathrm{𝗌𝗎𝗉}(a,f)))}\sum _{(\mathrm{𝗂𝗇𝖽}:{\prod }_{(w:W)}E(w))}\prod _{(a,f)}\\ \hfill \mathrm{𝗂𝗇𝖽}(\mathrm{𝗌𝗎𝗉}(a,f))=e(a,\lambda b.\mathrm{𝗂𝗇𝖽}(f(b))).\end{array}$$

In http://planetmath.org/node/87579Chapter 6 we will see some other reasons why propositional computation rules are worth considering.

In this section, we will state some basic facts about homotopy-inductive types. We omit most of the proofs, which are somewhat technical.

Theorem 5.5.1.

For any $A\mathrm{:}\mathrm{U}$ and $B\mathrm{:}A\mathrm{\to }\mathrm{U}$, the type ${\mathrm{W}}_d\mathit{}\mathrm{(}A\mathrm{,}B\mathrm{)}$ is a mere proposition.

It turns out that there is an equivalent characterization of $𝖶$-types using a recursion principle, plus certain uniqueness and coherence laws. First we give the recursion principle:

• When constructing a function from the $𝖶$-type ${𝖶}_{(x:A)}^{h}B(x)$ into the type $C$, it suffices to give its value for $\mathrm{𝗌𝗎𝗉}(a,f)$, assuming we are given the values of all $f(b)$ with $b:B(a)$. In other words, it suffices to construct a function

  $$c:\prod _{a:A}(B(a)\to C)\to C.$$

The associated computation rule for ${\mathrm{𝗋𝖾𝖼}}_{{𝖶}_{(x:A)}^{h}B(x)}(C,c):({𝖶}_{(x:A)}B(x))\to C$ is as follows:

• For any $a:A$ and $f:B(a)\to {𝖶}_{(x:A)}^{h}B(x)$ we have a witness $\beta (C,c,a,f)$ for equality

  $${\mathrm{𝗋𝖾𝖼}}_{{𝖶}_{(x:A)}^{h}B(x)}(C,c,\mathrm{𝗌𝗎𝗉}(a,f))=c(a,\lambda b.{\mathrm{𝗋𝖾𝖼}}_{{𝖶}_{(x:A)}^{h}B(x)}(C,c,f(b))).$$

Furthermore, we assert the following uniqueness principle, saying that any two functions defined by the same recurrence are equal:

• Let $C:𝒰$ and $c:{\prod }_{(a:A)}(B(a)\to C)\to C$ be given. Let $g,h:({𝖶}_{(x:A)}^{h}B(x))\to C$ be two functions which satisfy the recurrence $c$ up to propositional equality, i.e., such that we have

  ${\beta }_g$ $:{\displaystyle \prod _{a,f}}g(\mathrm{𝗌𝗎𝗉}(a,f))=c(a,\lambda b.g(f(b))),$

  ${\beta }_h$ $:{\displaystyle \prod _{a,f}}h(\mathrm{𝗌𝗎𝗉}(a,f))=c(a,\lambda b.h(f(b))).$

  Then $g$ and $h$ are equal, i.e. there is $\alpha (C,c,f,g,{\beta }_g,{\beta }_h)$ of type $g=h$.

Recall that when we have an induction principle rather than only a recursion principle, this propositional uniqueness principle is derivable (Theorem 5.3.1 (http://planetmath.org/53wtypes#Thmprethm1)). But with only recursion, the uniqueness principle is no longer derivable — and in fact, the statement is not even true (exercise). Hence, we postulate it as an axiom. We also postulate the following coherence law, which tells us how the proof of uniqueness behaves on canonical elements:

• For any $a:A$ and $f:B(a)\to C$, the following diagram commutes propositionally:

  HoTT_fig_5.5.1.png

  where $\alpha$ abbreviates the path $\alpha (C,c,f,g,{\beta }_g,{\beta }_h):g=h$.

Putting all of this data together yields another characterization of ${𝖶}_{(x:A)}B(x)$, as a type with a supremum function, satisfying simple elimination, computation, uniqueness, and coherence rules:

$$\begin{array}{c}{𝖶}_s(A,B):\equiv \sum _{W:𝒰}\sum _{\mathrm{𝗌𝗎𝗉}:{\prod }_{(a)}(B(a)\to W)\to W}\prod _{C:𝒰}\prod _{c:{\prod }_{(a)}(B(a)\to C)\to C}\sum _{\mathrm{𝗋𝖾𝖼}:W\to C}\hfill \\ \hfill \sum _{\beta :{\prod }_{(a,f)}\mathrm{𝗋𝖾𝖼}(\mathrm{𝗌𝗎𝗉}(a,f))=c(a,\lambda b.\mathrm{𝗋𝖾𝖼}(f(b)))}\prod _{g:W\to C}\prod _{h:W\to C}\prod _{{\beta }_g:{\prod }_{(a,f)}g(\mathrm{𝗌𝗎𝗉}(a,f))=c(a,\lambda b.g(f(b)))}\\ \hfill \prod _{{\beta }_h:{\prod }_{(a,f)}h(\mathrm{𝗌𝗎𝗉}(a,f))=c(a,\lambda b.h(f(b)))}\sum _{\alpha :{\prod }_{(w:W)}g(w)=h(w)}\\ \hfill \alpha (\mathrm{𝗌𝗎𝗉}(x,f)){\beta }_h={\beta }_{g}c(a,-)(\mathrm{𝖿𝗎𝗇𝖾𝗑𝗍}\lambda b.\alpha (f(b)))\end{array}$$

Theorem 5.5.2.

For any $A\mathrm{:}\mathrm{U}$ and $B\mathrm{:}A\mathrm{\to }\mathrm{U}$, the type ${\mathrm{W}}_s\mathit{}\mathrm{(}A\mathrm{,}B\mathrm{)}$ is a mere proposition.

Finally, we have a third, very concise characterization of ${𝖶}_{(x:A)}B(x)$ as an h-initial $𝖶$-algebra:

$${𝖶}_h(A,B):\equiv \sum _{I:\mathrm{𝖶𝖠𝗅𝗀}(A,B)}{\mathrm{𝗂𝗌𝖧𝗂𝗇𝗂𝗍}}_{𝖶}(A,B,I).$$

Theorem 5.5.3.

For any $A\mathrm{:}\mathrm{U}$ and $B\mathrm{:}A\mathrm{\to }\mathrm{U}$, the type ${\mathrm{W}}_h\mathit{}\mathrm{(}A\mathrm{,}B\mathrm{)}$ is a mere proposition.

It turns out all three characterizations of $𝖶$-types are in fact equivalent:

Lemma 5.5.4.

For any $A\mathrm{:}\mathrm{U}$ and $B\mathrm{:}A\mathrm{\to }\mathrm{U}$, we have

$${𝖶}_d(A,B)\simeq {𝖶}_s(A,B)\simeq {𝖶}_h(A,B)$$

Indeed, we have the following theorem, which is an improvement over Theorem 5.4.7 (http://planetmath.org/54inductivetypesareinitialalgebras#Thmprethm3):

Theorem 5.5.5.

The types satisfying the formation, introduction, elimination, and propositional computation rules for $\mathrm{W}$-types are precisely the homotopy-initial $\mathrm{W}$-algebras.

Sketch of proof.

Inspecting the proof of Theorem 5.4.7 (http://planetmath.org/54inductivetypesareinitialalgebras#Thmprethm3), we see that only the propositional computation rule was required to establish the h-initiality of ${𝖶}_{(x:A)}B(x)$. For the converse implication, let us assume that the polynomial functor associated to $A:𝒰$ and $B:A\to 𝒰$, has an h-initial algebra $(W,s_W)$; we show that $W$ satisfies the propositional rules of $𝖶$-types. The $𝖶$-introduction rule is simple; namely, for $a:A$ and $t:B(a)\to W$, we define $\mathrm{𝗌𝗎𝗉}(a,t):W$ to be the result of applying the structure map $s_W:PW\to W$ to $(a,t):PW$. For the $𝖶$-elimination rule, let us assume its premisses and in particular that $C^{\prime }:W\to 𝒰$. Using the other premisses, one shows that the type $C:\equiv {\sum }_{(w:W)}{C}^{\prime }(w)$ can be equipped with a structure map $s_C:PC\to C$. By the h-initiality of $W$, we obtain an algebra homomorphism $(f,s_f):(W,s_W)\to (C,s_C)$. Furthermore, the first projection ${\mathrm{𝗉𝗋}}_1:C\to W$ can be equipped with the structure of a homomorphism, so that we obtain a diagram of the form

HoTT_fig_5.5.2.png

But the identity function $1_W:W\to W$ has a canonical structure of an algebra homomorphism and so, by the contractibility of the type of homomorphisms from $(W,s_W)$ to itself, there must be an identity proof between the composite of $(f,s_f)$ with $({\mathrm{𝗉𝗋}}_1,s_{{\mathrm{𝗉𝗋}}_1})$ and $(1_W,s_{1_W})$. This implies, in particular, that there is an identity proof $p:{\mathrm{𝗉𝗋}}_1\circ f=1_W$.

Since $({\mathrm{𝗉𝗋}}_2\circ f)w:C(({\mathrm{𝗉𝗋}}_1\circ f)w)$, we can define

$$\mathrm{𝗋𝖾𝖼}(w,c):\equiv p_{*}(({\mathrm{𝗉𝗋}}_2\circ f)w):C(w)$$

where the transport $p_{*}$ is with respect to the family

$$\lambda u.C\circ u:(W\to W)\to W\to 𝒰.$$

The verification of the propositional $𝖶$-computation rule is a calculation, involving the naturality properties of operations of the form $p_{*}$. ∎

Finally, as desired, we can encode homotopy-natural-numbers as homotopy-$𝖶$-types:

Theorem 5.5.6.

The rules for natural numbers with propositional computation rules can be derived from the rules for $\mathrm{W}$-types with propositional computation rules.

Title	5.5 Homotopy-inductive types