Homotopy-Initial Algebras in Type Theory
Abstract
We investigate inductive types in type theory, using the insights provided by homotopy type theory and univalent foundations of mathematics. We do so by introducing the new notion of a homotopy-initial algebra. This notion is defined by a purely type-theoretic contractibility condition that replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterizes the types that are equivalent to W-types as homotopy-initial algebras.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 30, 2017
- Source ID
- 10.1145/3006383
Entities
People
- Kristina Sojakova
- Nicola Gambino
- Steve Awodey
Organizations
- Air Force Research Laboratory
- Army Research Office
- Carnegie Mellon University
- Engineering and Physical Sciences Research Council
- John Templeton Foundation
- National Science Foundation
- University of Leeds