CMU-CS-14-101Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-14-101
Kristina Sojakova January 2014
Keywords:
Homotopy Type Theory, higher inductive types, homotopy-initial algebras
Homotopy Type Theory is a new field of mathematics based on the surprising and elegant correspondence between Martin-Löf's constructive type theory and abstract homotopy theory. We have a powerful interplay between these disciplines - we can use geometric intuition to formulate new concepts in type theory and, conversely, use type-theoretic machinery to verify and often simplify existing mathematical proofs. A crucial ingredient in this new system are higher inductive types, which allow us to represent objects such as spheres, tori, pushouts, and quotients. We investigate a variant of higher inductive types whose computational behavior is determined up to a higher path. We show that in this setting, higher inductive types are characterized by the universal property of being a homotopy-initial algebra. 51 pages
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |