skip to main content
research-article

Higher Inductive Types as Homotopy-Initial Algebras

Published: 14 January 2015 Publication History

Abstract

Homotopy 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 intuition to formulate new concepts in type theory and, conversely, use type-theoretic machinery to verify and often simplify existing mathematical proofs.
Higher inductive types form a crucial part of this new system since they allow us to represent mathematical objects, such as spheres, tori, pushouts, and quotients, in the type theory. We investigate a class of higher inductive types called W-suspensions which generalize Martin-Löf's well-founded trees. We show that a propositional variant of W-suspensions, whose computational behavior is determined up to a higher path, is characterized by the universal property of being a homotopy-initial algebra. As a corollary we get that W-suspensions in the strict form are homotopy-initial.

Supplementary Material

MOV File (2676983.mov)

References

[1]
S. Awodey and A. Bauer. Propositions as {types}. Journal of Logic and Computation, 14(4):447--471, 2004.
[2]
S. Awodey and M. Warren. Homotopy-theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1):45--55, 2009.
[3]
S. Awodey, N. Gambino, and K. Sojakova. Inductive types in Homotopy Type Theory. In Logic in Computer Science (LICS 2012), pages 95--104. IEEE Computer Society, 2012.
[4]
M. Bezem, T. Coquand, and S. Huber. A model of type theory in cubical sets, 2014. Available at http://www.cse.chalmers.se/~coquand/mod1.pdf.
[5]
Coq Development Team. The Coq Proof Assistant Reference Manual, version 8.4pl3. INRIA, 2012. Available at coq.inria.fr.
[6]
N. Gambino and R. Garner. The identity type weak factorisation system. Theoretical Computer Science, 409(3):94--109, 2008.
[7]
R. Garner. Two-dimensional models of type theory. Mathematical Structures in Computer Science, 19(4):687--736, 2009.
[8]
M. Hofmann and T. Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory 1995, volume 36 of Oxford Logic Guides, pages 83--111. Oxford Univ. Press, 1998.
[9]
C. Kapulkin, P. Lumsdaine, and V. Voevodsky. The simplicial model of univalent foundations. Available as arXiv:1211.2851v1, 2012.
[10]
N. Kraus. The truncation map |_| : N -- ||N|| is nearly invertible, 2013. Post on the Homotopy Type Theory blog.
[11]
D. Licata and G. Brunerie. πnSn) in Homotopy Type Theory. In Certified Programs and Proofs, volume 8307 of LNCS, pages 1--16. Springer, 2013.
[12]
D. Licata and R. Harper. Canonicity for 2-dimensional type theory. In Principles of Programming Languages (POPL 2012), pages 337--348. ACM, 2012.
[13]
D. Licata and M. Shulman. Calculating the fundamental group of the circle in Homotopy Type Theory. In Logic in Computer Science (LICS 2013), pages 223--232. IEEE Computer Society, 2013.
[14]
P. Lumsdaine. Weak ω-categories from intensional type theory. Logical Methods in Computer Science, 6:1--19, 2010.
[15]
P. Lumsdaine. Higher inductive types: a tour of the menagerie, 2011. Post on the Homotopy Type Theory blog.
[16]
P. Lumsdaine and M. Shulman. Semantics of higher inductive types, 2012. Available at http://uf-ias-2012.wikispaces.com/file/view/semantics.pdf.
[17]
P. Martin-Löf. An intuitionistic theory of types: Predicative part. In Logic Colloquium 1973, pages 73--118. North-Holland, 1975.
[18]
P. Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology, and Philosophy of Science, pages 153--175. North-Holland, 1982.
[19]
U. Norell. Towards a practical programming language based on de- pendent type theory. PhD thesis, Chalmers University of Technology, 2007.
[20]
M. Shulman. Homotopy Type Theory, VI, 2011. Post on the n- category cafe blog.
[21]
K. Sojakova. Higher inductive types as homotopy-initial algebras. Technical Report Carnegie Mellon University-CS-14--101R, Carnegie Mellon University, 2014. Available at http://reports-archive.adm.cs.cmu.edu/.
[22]
T. Streicher. Investigations into intensional type theory. Habilitation Thesis. Available from the authors web page, 1993.
[23]
The Univalent Foundations Program, Institute for Advanced Study. Homotopy Type Theory - Univalent Foundations of Mathematics. Univalent Foundations Project, 2013.
[24]
B. van den Berg and R. Garner. Types are weak ε-groupoids. London Mathematical Society, 102(2):370--394, 2011.
[25]
B. van den Berg and R. Garner. Topological and simplicial models of identity types. ACM TOCL, 13(1), 2012.
[26]
V. Voevodsky. Univalent foundations of mathematics, 2011. Invited talk at the Workshop on Logic, Language, Information and Computation (WoLLIC 2011).
[27]
M. Warren. Homotopy-theoretic aspects of constructive type theory. PhD thesis, Carnegie Mellon University, 2008.

Cited By

View all
  • (2022)Greatest HITs: Higher inductive types in coinductive definitions via induction under clocksProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533359(1-13)Online publication date: 2-Aug-2022
  • (2019)Path spaces of higher inductive types in homotopy type theoryProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470159(1-13)Online publication date: 24-Jun-2019
  • (2024)The Compatibility of the Minimalist Foundation with Homotopy Type TheoryTheoretical Computer Science10.1016/j.tcs.2024.114421(114421)Online publication date: Feb-2024
  • Show More Cited By

Index Terms

  1. Higher Inductive Types as Homotopy-Initial Algebras

      Recommendations

      Comments

      Information & Contributors

      Information

      Published In

      cover image ACM SIGPLAN Notices
      ACM SIGPLAN Notices  Volume 50, Issue 1
      POPL '15
      January 2015
      682 pages
      ISSN:0362-1340
      EISSN:1558-1160
      DOI:10.1145/2775051
      • Editor:
      • Andy Gill
      Issue’s Table of Contents
      • cover image ACM Conferences
        POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
        January 2015
        716 pages
        ISBN:9781450333009
        DOI:10.1145/2676726
      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      Published: 14 January 2015
      Published in SIGPLAN Volume 50, Issue 1

      Check for updates

      Author Tags

      1. higher inductive type
      2. homotopy type theory
      3. homotopy-initial algebra
      4. w-suspension

      Qualifiers

      • Research-article

      Contributors

      Other Metrics

      Bibliometrics & Citations

      Bibliometrics

      Article Metrics

      • Downloads (Last 12 months)18
      • Downloads (Last 6 weeks)4
      Reflects downloads up to 19 Feb 2025

      Other Metrics

      Citations

      Cited By

      View all
      • (2022)Greatest HITs: Higher inductive types in coinductive definitions via induction under clocksProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533359(1-13)Online publication date: 2-Aug-2022
      • (2019)Path spaces of higher inductive types in homotopy type theoryProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470159(1-13)Online publication date: 24-Jun-2019
      • (2024)The Compatibility of the Minimalist Foundation with Homotopy Type TheoryTheoretical Computer Science10.1016/j.tcs.2024.114421(114421)Online publication date: Feb-2024
      • (2022)A class of higher inductive types in Zermelo‐Fraenkel set theoryMathematical Logic Quarterly10.1002/malq.20210004068:1(118-127)Online publication date: 9-Feb-2022
      • (2020)Constructing Higher Inductive Types as Groupoid QuotientsProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394803(929-943)Online publication date: 8-Jul-2020
      • (2020)Sequential Colimits in Homotopy Type TheoryProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394801(845-858)Online publication date: 8-Jul-2020
      • (2020)Large and Infinitary Quotient Inductive-Inductive TypesProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3373718.3394770(648-661)Online publication date: 8-Jul-2020
      • (2020)Constructing Infinitary Quotient-Inductive TypesFoundations of Software Science and Computation Structures10.1007/978-3-030-45231-5_14(257-276)Online publication date: 25-Apr-2020
      • (2019)Constructing quotient inductive-inductive typesProceedings of the ACM on Programming Languages10.1145/32903153:POPL(1-24)Online publication date: 2-Jan-2019
      • (2019)Higher inductive types in cubical computational type theoryProceedings of the ACM on Programming Languages10.1145/32903143:POPL(1-27)Online publication date: 2-Jan-2019
      • Show More Cited By

      View Options

      Login options

      View options

      PDF

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader

      Figures

      Tables

      Media

      Share

      Share

      Share this Publication link

      Share on social media