Document Open Access Logo

For Finitary Induction-Induction, Induction Is Enough

Authors Ambrus Kaposi , András Kovács , Ambroise Lafont

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2019.6.pdf
  • Filesize: 0.59 MB
  • 30 pages

Document Identifiers

Author Details

Ambrus Kaposi
  • Eötvös Loránd University, Budapest, Hungary
András Kovács
  • Eötvös Loránd University, Budapest, Hungary
Ambroise Lafont
  • IMT Atlantique, Inria, LS2N CNRS, Nantes, France

Funding

  • Kaposi, Ambrus: this author was supported by the National Research, Development and Innovation Fund of Hungary, financed under the Thematic Excellence Programme funding scheme, Project no. ED_18-1-2019-0030, by the New National Excellence Program of the Ministry for Innovation and Technology, Project no. ÚNKP-19-4-ELTE-874, and by the Bolyai Fellowship of the Hungarian Academy of Sciences, Project no. BO/00659/19/3.
  • Kovács, András: this author was supported by the European Union, co-financed by the European Social Fund (EFOP-3.6.3-VEKOP-16-2017-00002).
  • Lafont, Ambroise: this author was supported by the CoqHoTT ERC Grant 637339.

Acknowledgements

The authors would like to thank Thorsten Altenkirch, Rafaël Bocquet, Simon Boulier, Fredrik Nordvall-Forsberg and Jakob von Raumer for discussions on the topics of this paper. We also thank the anonymous reviewers for their helpful comments and suggestions.

Cite AsGet BibTex

Ambrus Kaposi, András Kovács, and Ambroise Lafont. For Finitary Induction-Induction, Induction Is Enough. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 6:1-6:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.TYPES.2019.6

Abstract

Inductive-inductive types (IITs) are a generalisation of inductive types in type theory. They allow the mutual definition of types with multiple sorts where later sorts can be indexed by previous ones. An example is the Chapman-style syntax of type theory with conversion relations for each sort where e.g. the sort of types is indexed by contexts. In this paper we show that if a model of extensional type theory (ETT) supports indexed W-types, then it supports finitely branching IITs. We use a small internal type theory called the theory of signatures to specify IITs. We show that if a model of ETT supports the syntax for the theory of signatures, then it supports all IITs. We construct this syntax from indexed W-types using preterms and typing relations and prove its initiality following Streicher. The construction of the syntax and its initiality proof were formalised in Agda.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • type theory
  • inductive types
  • inductive-inductive types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Benedikt Ahrens, Ralph Matthes, and Anders Mörtberg. From signatures to monads in unimath. Journal of Automated Reasoning, 63(2):285-318, August 2019. URL: https://doi.org/10.1007/s10817-018-9474-4.
  2. Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg. Quotient inductive-inductive types. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures, pages 293-310, Cham, 2018. Springer International Publishing. Google Scholar
  3. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. Indexed containers. J. Funct. Program., 25, 2015. URL: https://doi.org/10.1017/S095679681500009X.
  4. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Rastislav Bodik and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 18-29. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837638.
  5. Thorsten Altenkirch, Ambrus Kaposi, András Kovács, and Jakob von Raumer. Constructing inductive-inductive types via type erasure. In Marc Bezem, editor, 25th International Conference on Types for Proofs and Programs, TYPES 2019. Centre for Advanced Study at the Norwegian Academy of Science and Letters, 2019. Google Scholar
  6. Thorsten Altenkirch, Nuo Li, and Ondřej Rypáček. Some constructions on Ω-groupoids. In Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP '14, pages 4:1-4:8, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2631172.2631176.
  7. Robert Atkey, Neil Ghani, and Patricia Johann. A relationally parametric model of dependent type theory. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, page 503–515, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2535838.2535852.
  8. Steve Awodey, Jonas Frey, and Sam Speight. Impredicative encodings of (higher) inductive types. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 76-85. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209130.
  9. Andrej Bauer, Philipp G. Haselwarter, and Théo Winterhalter. A modular formalization of type theory in Coq. In Ambrus Kaposi, editor, 23rd International Conference on Types for Proofs and Programs, TYPES 2017. Eötvös Loránd University, 2017. Google Scholar
  10. Guillaume Brunerie. A formalization of the initiality conjecture in agda. Slides of a talk at the Homotopy Type Theory 2019 Conference, Carnegie Mellon University, Pittsburgh, Pennsylvania, August 2019. URL: https://guillaumebrunerie.github.io/pdf/initiality.pdf.
  11. Paolo Capriotti. Notions of type formers. In Ambrus Kaposi, editor, 23rd International Conference on Types for Proofs and Programs, TYPES 2017. Eötvös Loránd University, 2017. Google Scholar
  12. John Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209-243, 1986. Google Scholar
  13. James Chapman. Type theory should eat itself. Electronic Notes in Theoretical Computer Science, 228:21-36, January 2009. URL: https://doi.org/10.1016/j.entcs.2008.12.114.
  14. Jesper Cockx and Andreas Abel. Sprinkles of extensionality for your vanilla type theory. In Silvia Ghilezan and Ivetić Jelena, editors, 22nd International Conference on Types for Proofs and Programs, TYPES 2016. University of Novi Sad, 2016. Google Scholar
  15. Nils Anders Danielsson. A formalisation of a dependently typed language as an inductive-recursive family. In Thorsten Altenkirch and Conor McBride, editors, TYPES, volume 4502 of Lecture Notes in Computer Science, pages 93-109. Springer, 2006. URL: https://doi.org/10.1007/978-3-540-74464-1_7.
  16. Peter Dybjer. Internal type theory. In Lecture Notes in Computer Science, pages 120-134. Springer, 1996. Google Scholar
  17. Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In Typed Lambda Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, pages 129-146. Springer, 1999. Google Scholar
  18. Martin Hofmann. Syntax and semantics of dependent types. In Semantics and Logics of Computation, pages 79-130. Cambridge University Press, 1997. Google Scholar
  19. Jasper Hugunin. Constructing inductive-inductive types in cubical type theory. In Mikołaj Bojańczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures, pages 295-312, Cham, 2019. Springer International Publishing. Google Scholar
  20. Ambrus Kaposi. Re: separate definition of constructors? Email to the Agda mailing list, May 2019. URL: https://lists.chalmers.se/pipermail/agda/2019/011176.html.
  21. Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing quotient inductive-inductive types. Proc. ACM Program. Lang., 3(POPL):2:1-2:24, January 2019. URL: https://doi.org/10.1145/3290315.
  22. Ambrus Kaposi, András Kovács, and Ambroise Lafont. Closed inductive-inductive types are reducible to indexed inductive types. In Marc Bezem, editor, 25th International Conference on Types for Proofs and Programs, TYPES 2019. Centre for Advanced Study at the Norwegian Academy of Science and Letters, 2019. Google Scholar
  23. Ambrus Kaposi and Jakob von Raumer. A syntax for mutual inductive families. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), 2020. To appear. Google Scholar
  24. András Kovács and Ambrus Kaposi. Large and infinitary quotient inductive-inductive types. In 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020, Saarbrücken, Germany, July 8-11, 2020, 2020. To appear. Google Scholar
  25. Lorenzo Malatesta, Thorsten Altenkirch, Neil Ghani, Peter Hancock, and Conor McBride. Small induction recursion, indexed containers and dependent polynomials are equivalent, 2013. TLCA 2013. Google Scholar
  26. Fredrik Nordvall Forsberg. Inductive-inductive definitions. PhD thesis, Swansea University, 2013. Google Scholar
  27. Fredrik Nordvall Forsberg and Anton Setzer. Inductive-inductive definitions. In Anuj Dawar and Helmut Veith, editors, CSL 2010, volume 6247 of Lecture Notes in Computer Science, pages 454-468. Springer, Heidelberg, 2010. Google Scholar
  28. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007. Google Scholar
  29. The Univalent Foundations Program. Homotopy type theory: Univalent foundations of mathematics. Technical report, Institute for Advanced Study, 2013. Google Scholar
  30. Thomas Streicher. Semantics of Type Theory: Correctness, Completeness, and Independence Results. Birkhauser Boston Inc., Cambridge, MA, USA, 1991. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact