Impredicative Encodings of Inductive Types in HoTT

Homotopy Type Theory

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

$latex forall X. (Xrightarrow X) rightarrow X rightarrow X,$

of natural numbers do not satisfy the relevant $latex 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 $latex 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 $latex Xmapsto X+mathbf{1}$.

For the inductive types treated in the thesis, we do not use the full power of HoTT; we need only postulate $latex Sigma$-types…

View original post 833 more words

This entry was posted in Philosophie. Bookmark the permalink.