Homotopy-initial algebras in type theory
Logic
2015-04-22 v1 Category 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 which replaces the standard, category-theoretic universal property involving the existence and uniqueness of appropriate morphisms. Our main result characterises the types that are equivalent to W-types as homotopy-initial algebras.
Cite
@article{arxiv.1504.05531,
title = {Homotopy-initial algebras in type theory},
author = {Steve Awodey and Nicola Gambino and Kristina Sojakova},
journal= {arXiv preprint arXiv:1504.05531},
year = {2015}
}
Comments
supersedes arXiv:1201.3898