Steve Awodey
Skip Abstract Section
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.
- M. Abbott, T. Altenkirch, and N. Ghani. 2005. Containers: Constructing strictly positive types. Theoretical Computer Science 342, 1 (2005), 3--27. Google Scholar
Digital Library
- P. Aczel. 2014. The structure identity principle and the univalence axiom. The Bulletin of Symbolic Logic 342, 3 (2014), 376.Google Scholar
- S. Awodey and A. Bauer. 2004. Propositions as [types]. Journal of Logic and Computation 14, 4 (2004), 447--471. Google ScholarDigital Library
- S. Awodey, N. Gambino, and K. Sojakova. 2012. Inductive types in homotopy type theory. In Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS’12). IEEE Computer Society, 95--104. Google ScholarDigital Library
- S. Awodey and M. Warren. 2009. Homotopy-theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society 146, 1 (2009), 45--55. Google ScholarCross Ref
- Y. Bertot and P. Castéran. 2004. Interactive Theorem Proving and Program Development. Coq’Art: the Calculus of Inductive Constructions. Springer-Verlag. Google ScholarCross Ref
- R. Blackwell, G. M. Kelly, and A. J. Power. 1989. Two-dimensional monad theory. Journal of Pure and Applied Algebra 59, 1 (1989), 1--41. Google ScholarCross Ref
- M. Boardman and R. Vogt. 1973. Homotopy-Invariant Algebraic Structures on Topological Spaces. Number 347 in Lecture Notes in Mathematics. Springer-Verlag. Google ScholarCross Ref
- T. Coquand and C. Paulin-Mohring. 1990. Inductively defined types. In International Conference on Computer Logic (COLOG’88), Lecture Notes in Computer Science, Vol. 417. Springer, 50--66. Google ScholarCross Ref
- P. Dybjer. 1997. Representing inductively defined sets by well-orderings in Martin-Löf’s type theory. Theoretical Computer Science 176 (1997), 329--335. Google ScholarDigital Library
- N. Gambino and R. Garner. 2008. The identity type weak factorisation system. Theoretical Computer Science 409, 3 (2008), 94--109. Google ScholarDigital Library
- N. Gambino and M. Hyland. 2004. Well-founded trees and dependent polynomial functors. In Types for Proofs and Programs (TYPES’03), Lecture Notes in Computer Science, Vol. 3085, S. Berardi, M. Coppo, and F. Damiani (Eds.). Springer, 210--225. Google ScholarCross Ref
- H. Goguen and Z. Luo. 1993. Inductive data types: Well-ordering types revisited. In Logical Environments, G. Huet and G. Plotkin (Eds.). Cambridge University Press, 198--218.Google Scholar
- M. Hofmann. 1997. Extensional Constructs in Intensional Type Theory. Springer-Verlag. Google ScholarCross Ref
- M. Hofmann and T. Streicher. 1998. The groupoid interpretation of type theory. In Twenty-Five Years of Constructive Type Theory 1995 (Oxford Logic Guides), Vol. 36. Oxford University Press, 83--111.Google Scholar
- A. Joyal. 2014. Categorical homotopy type theory. Slides of a seminar given at MIT. (2014). Available from http://ncatlab.org/homotopytypetheory/files/Joyal.pdf.Google Scholar
- C. Kapulkin and P. LeFanu Lumsdaine. 2016. The Simplicial Model of Univalent Foundations (after Voevodsky). (2016). arXiv:1211.2851v4.Google Scholar
- J. Kock. 2012. Data types with symmetries and polynomial functors over groupoids. Electronic Notes in Theoretical Computer Science 286 (2012), 351--365. Google ScholarDigital Library
- F. W. Lawvere. 1964. An elementary theory of the category of sets. Proceedings of the National Academy of Sciences 52, 6 (1964), 1506--11. Google ScholarCross Ref
- P. LeFanu Lumsdaine. 2010a. Higher Categories from Type Theories. Ph.D. dissertation. Carnegie Mellon University.Google Scholar
- P. LeFanu Lumsdaine. 2010b. Weak ω-categories from intensional type theory. Logical Methods in Computer Science 6 (2010), 1--19.Google Scholar
- P. LeFanu Lumsdaine. 2011. Higher inductive types: A tour of the menagerie. (2011). Post on the Homotopy Type Theory blog.Google Scholar
- J. Lurie. 2009. Higher Topos Theory. Princeton University Press.Google Scholar
- P. Martin-Löf. 1975. An intuitionistic theory of types: Predicative part. In Logic Colloquium 1973, H. Rose and J. Shepherdson (Eds.). North-Holland, 73--118.Google Scholar
- P. Martin-Löf. 1984. Intuitionistic Type Theory. Notes by G. Sambin of a series of lectures given in Padua, 1980. (1984). Bibliopolis.Google Scholar
- I. Moerdijk and E. Palmgren. 2000. Well-founded trees in categories. Annals of Pure and Applied Logic 104 (2000), 189--218. Google ScholarCross Ref
- B. Nordström, K. Petersson, and J. Smith. 1990. Programming in Martin-Löf Type Theory. Oxford University Press.Google Scholar
- B. Nordström, K. Petersson, and J. Smith. 2000. Martin-Löf type theory. In Handbook of Logic in Computer Science, Vol. 5. Oxford University Press, 1--37.Google Scholar
- C. Paulin-Mohring. 1993. Inductive definitions in the system Coq—Rules and properties. In Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA’93), Vol. 664. Springer, 328--345. Google ScholarCross Ref
- K. Petersson and D. Synek. 1989. A set constructor for inductive sets in Martin-Löfs type theory. In Category Theory and Computer Science, Lecture Notes in Computer Science, Vol. 389. Springer-Verlag, 128--140. Google ScholarCross Ref
- M. Shulman. 2011. Homotopy Type Theory, VI. (2011). Post on the n-category cafe blog.Google Scholar
- K. Sojakova. 2014. Higher Inductive Types as Homotopy-Initial Algebras. Technical Report CMU-CS-14-101R. Carnegie Mellon University. Available at http://reports-archive.adm.cs.cmu.edu/.Google Scholar
- K. Sojakova. 2015. Higher inductive types as homotopy-initial algebras. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’15). ACM, 31--42. Google ScholarDigital Library
- K. Sojakova. 2016. Higher Inductive Types as Homotopy-initial Algebras. Ph.D. dissertation. Carnegie Mellon University.Google Scholar
- T. Streicher. 1993. Investigations into intensional type theory. Habilitation thesis, Ludwig-Maximilans-Universität München.Google Scholar
- The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study.Google Scholar
- B. van den Berg and R. Garner. 2011. Types are weak ω-groupoids. Journal of the London Mathematical Society 102, 2 (2011), 370--394. Google ScholarCross Ref
- B. van den Berg and I. Moerdijk. 2015. W-types in homotopy type theory. Mathematical Structures in Computer Science 25, 5 (2015), 1100--1115. Google ScholarCross Ref
- V. Voevodsky. 2009. Notes on type systems. (2009). Unpublished paper.Google Scholar
- V. Voevodsky. 2014. The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010). arXiv:1402.5556v2.Google Scholar
- V. Voevodsky. 2015. An experimental library of formalized mathematics based on the univalent foundations. Mathematical Structures in Computer Science 25, 5 (2015), 1278--1294. Google ScholarCross Ref
Index Terms
- Homotopy-Initial Algebras in Type Theory
Recommendations
Higher Inductive Types as Homotopy-Initial Algebras
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesHomotopy Type Theory is a new field of mathematics based on the recently-discovered 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 ...
Containers: constructing strictly positive types
Applied semantics: Selected topicsWe introduce the notion of a Martin-Löf category--a locally cartesian closed category with disjoint coproducts and initial algebras of container functors (the categorical analogue of W-types)--and then establish that nested strictly positive inductive ...
A functional programmer's guide to homotopy type theory
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional ProgrammingDependent type theories are functional programming languages with types rich enough to do computer-checked mathematics and software verification. Homotopy type theory is a recent area of work that connects dependent type theory to the mathematical ...
Comments