Impredicative Encodings of Inductive Types in HoTT

I recently completed my master’s thesis under the supervision of Steve Awodey and Jonas Frey. A copy can be found here.

Known impredicative encodings of various inductive types in System F, such as the type

$\forall X. (X\rightarrow X) \rightarrow X \rightarrow X,$

of natural numbers do not satisfy the relevant $\eta$ -computation rules. The aim of this work is to refine the System F encodings by moving to a system of HoTT with an impredicative universe, so that the relevant $\eta$ -rules are satisfied (along with all the other rules). As a result, the so-determined types have their expected universal properties. The main result is the construction of a type of natural numbers which is the initial algebra for the expected endofunctor $X\mapsto X+\mathbf{1}$ .

For the inductive types treated in the thesis, we do not use the full power of HoTT; we need only postulate $\Sigma$ -types, identity types, “large” $\Pi$ -types over an impredicative universe $\mathcal{U}$ and function extensionality. Having large $\Pi$ -types over an impredicative universe $\mathcal{U}$ means that given a type $\Gamma\vdash A \:\mathsf{type}$ and a type family $\Gamma, x:A \vdash B:\mathcal{U}$ , we may form the dependent function type

$\displaystyle{ \Gamma\vdash \prod_{x:A} B:\mathcal{U}}.$

Note that this type is in $\mathcal{U}$ even if $A$ is not.

We obtain a translation of System F types into type theory by replacing second order quantification by dependent products over $\mathcal U$ (or alternatively over the subtype of $\mathcal{U}$ given by some h-level).

For brevity, we will focus on the construction of the natural numbers (though in the thesis, the coproduct of sets and the unit type is first treated with special cases of this method). We consider categories of algebras for endofunctors:

$T:\mathbf{Set}\rightarrow\mathbf{Set},$

where the type of objects of $\mathbf{Set}$ is given by

$\mathsf{Set} :\equiv \displaystyle{\sum_{X:\mathcal{U}}}\mathsf{isSet}(X),$

(the type of sets (in $\mathcal{U}$ )) and morphisms are simply functions between sets.

We can write down the type of $T$ -algebras:

$\mathsf{TAlg} :\equiv \displaystyle{\sum_{X:\mathsf{Set}}} T(X)\rightarrow X$

and homomorphisms between algebras $\phi$ and $\psi$ :

$\mathsf{THom}(\phi,\psi) :\equiv \displaystyle{\sum_{f:\mathsf{pr_1}(\phi)\rightarrow\mathsf{pr_1}(\psi)}} \mathsf{pr_2}(\psi) \circ T(f) = f \circ \mathsf{pr_2}(\phi),$

which together form the category $\mathbf{TAlg}$ .

We seek the initial object in $\mathbf{TAlg}$ . Denote this by $0$ and moreover let $U$ be the forgetful functor to $\mathbf{Set}$ and $y:\mathbf{TAlg}^{\textnormal{op}}\rightarrow \mathbf{Set}^{\mathbf{TAlg}}$ be the covariant Yoneda embedding. We reason as follows:

$U0 \cong \textnormal{Hom}_{\mathbf{Set}^\mathbf{TAlg}}(y0,U) \\{}\:\,\,\,\,\,\, = \textnormal{Hom}_{\mathbf{Set}^\mathbf{TAlg}}(1,U) \\{}\:\,\,\,\,\,\, = \textnormal{Hom}_{\mathbf{Set}^\mathbf{TAlg}}(\Delta 1,U) \\{}\:\,\,\,\,\,\, = \textnormal{Hom}_{\mathbf{Set}}(1, \textnormal{lim}_{\phi\in\textbf{TAlg}} U\phi) \\{}\:\,\,\,\,\,\, \cong \textnormal{lim}_{\phi\in\textbf{TAlg}} U\phi,$

using the fact that the diagonal functor is left adjoint to the limit functor for the last step. With this, we have a proposal for the definition of the underlying set of the initial $T$ -algebra as the limit of the forgetful functor. Using the fact that $U0$ is defined as a limit, we obtain an algebra structure $\epsilon:TU0\rightarrow U0$ . As $U$ creates limits, $(U0,\epsilon)$ is guaranteed to be initial in $\mathbf{TAlg}$ .

But we want to define $U0$ in type theory. We do this using products and equalizers as is well known from category theory. Explicitly, we take the equalizer of the following two maps between products:

$P_1,P_2 : \left(\displaystyle{\prod_{\phi:\mathbf{TAlg}}}U(\phi)\right) \rightarrow \displaystyle{\prod_{\phi,\psi:\mathbf{TAlg}}} \: \displaystyle{\prod_{\mu:\mathbf{THom}(\phi,\psi)}}U(\psi),$

given by:

$P_1 :\equiv \lambda\Phi.\lambda\phi.\lambda\psi.\lambda\mu.\Phi(\psi), \\ P_1 :\equiv \lambda\Phi.\lambda\phi.\lambda\psi.\lambda\mu. \mathsf{pr_1}(\mu)(\Phi(\phi)).$

The equalizer is, of course:

$E :\equiv \displaystyle{\sum_{\Phi : \prod_{(\phi:\mathbf{TAlg})} U(\phi)}} P_1(\Phi)=P_2(\Phi),$

which inhabits $\mathsf{Set}$ . Impredicativity is crucial for this: it guarantees that the product over $\mathbf{TAlg}$ lands in $\mathcal{U}$ .

This method can be used to construct an initial algebra, and therefore a fixed-point, for any endofunctor $T : \mathsf{Set}\rightarrow\mathsf{Set}\,$ ! We won’t pursue this remarkable fact here, but only consider the case at hand, where the functor $T$ is $X\mapsto X+\mathbf{1}$ . Then the equalizer $E$ becomes our definition of the type of natural numbers (so let us rename $E$ to $\mathbb{N}$ for the remainder). Observe that this encoding can be seen as a subtype of (a translation of) the System F encoding given at the start. Indeed, the indexing object $\prod_{(\phi:\mathbf{TAlg})} U(\phi)$ of $E$ is equivalent to $\prod_{(X:\mathbf{Set})}(X\rightarrow X)\rightarrow X \rightarrow X$ , by

$\begin{aligned} \quad\quad\displaystyle{\prod_{\phi:\mathbf{TAlg}}} U(\phi) \quad &\cong\quad \displaystyle{\prod_{\phi:{\displaystyle{\sum_{X:\mathsf{Set}}} T(X)\rightarrow X}}} U(\phi)\\ &\cong\quad \displaystyle{\prod_{X:\mathsf{Set}}}\, \displaystyle{\prod_{f:T(X)\rightarrow X}} X\\ &\cong\quad \displaystyle{\prod_{X:\mathsf{Set}}}\, (T(X)\rightarrow X) \rightarrow X\\ &\cong\quad \displaystyle{\prod_{X:\mathbf{Set}}}(X\rightarrow X)\rightarrow X \rightarrow X \,. \end{aligned}$

With this, we can define a successor function and zero element, for instance:

$0 :\equiv \left( \lambda\phi. \mathsf{pr_2}(\phi)\mathsf{inr}(\star), \lambda\phi.\lambda\psi.\lambda\mu. \mathsf{refl}_{\mathsf{pr_2}(\psi)\mathsf{inr}(\star)}\right)$

(the successor function takes a little more work). We can also define a recursor $\mathsf{rec}_{\mathbb{N}}(e,c)$ , given any $C:\mathsf{Set}, e:C\rightarrow C$ and $c:C$ . In other words, the introduction rules hold, and we can eliminate into other sets. Further, the $\beta$ -rules hold definitionally – as expected, since they hold for the System F encodings.

Finally we come to the desired result, the $\eta$ -rule for $\mathbb{N}$ :

Theorem. Let $C:\mathsf{Set}, e:C\rightarrow C$ and $c:C$ . Moreover, let $f:\mathbb{N}\rightarrow C$ such that:

$f(0)=c, \\ f(\mathsf{succ}(x) = e(f(x))$

for any $x:\mathbb{N}$ . Then

$\mathsf{rec}_{\mathbb{N}}(e,c) =f.$

Note that the $\eta$ -rule holds propositionally. By Awodey, Gambino, and Sojakova we therefore also have, equivalently, the induction principle for $\mathbb{N}$ , aka the dependent elimination rule. As a corollary, we can prove the universal property that any $T$ -algebra homomorphism is propositionally equal to the appropriate recursor (as a $T$ -algebra homomorphism). Again we emphasise the need for impredicativity: in the proof of $\eta$ , we have to be able to plug $\mathbb{N}$ into quantifiers over $\mathsf{Set}$ .

A semantic rendering of the above is that we have built a type that always determines a natural numbers object—whereas the System F encoding need not always do so (see Rummelhoff). In an appendix, we discuss a realizability semantics for the system we work in. Building more exotic types (that need not be sets) becomes more complicated; we leave this to future work.

5 Responses to Impredicative Encodings of Inductive Types in HoTT

Mike Shulman says:

13 October 2017 at 19:35

Neat! I notice that you only get a “natural numbers type” that can eliminate into sets. Can you say anything about whether it can eliminate into higher types?

Steve Awodey says:

16 October 2017 at 22:52

So here’s one idea: one can make higher encodings that quantify over n-types, but then one needs to add higher coherence conditions. Making $\mathbb{N}_n$ in this way still produces a 0-type (say, by Hedberg’s theorem), so one can then eliminate $\mathbb{N}_0$ into it, and from there into any n-type. In fact, one can presumably show that all the $\mathbb{N}_n$ s are equivalent. The catch is to actually write down the coherence laws required for n-types, which can be done “in principle”. Of course, this still doesn’t give elimination into types that are not n-truncated for some n.

- Mike Shulman says:
  
  17 October 2017 at 01:42
  
  Ah, yes, that makes sense. And maybe if the type theory had “limits of Reedy fibrant towers” you could impose all the coherence laws at once and get to untruncated types.
  
  - Steve Awodey says:
    
    17 October 2017 at 18:10
    
    yes, exactly.
    
Pingback: Impredicative Encodings, Part 3 | Homotopy Type Theory