12

Impredicative Encodings of Inductive Types in HoTT

 3 years ago
source link: https://homotopytypetheory.org/2017/10/11/impredicative-encodings-of-inductive-types-in-hott/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
neoserver,ios ssh client

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.


report

Recommend

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK