Quotients in Dependent Type Theory (Invited Talk)

Author Andrew M. Pitts



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.3.pdf
  • Filesize: 211 kB
  • 2 pages

Document Identifiers

Author Details

Andrew M. Pitts
  • Department of Computer Science & Technology, University of Cambridge, UK

Cite AsGet BibTex

Andrew M. Pitts. Quotients in Dependent Type Theory (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.3

Abstract

Constructs that involve taking a quotient are commonplace in mathematics. Here I will consider how they are treated within dependent type theory. The notion of quotient type has its origins in the Nuprl theorem-proving system [R. L. Constable et al., 1986] for extensional type theory. Later Hofmann formulated a version for intensional type theory in his thesis [M. Hofmann, 1995]. This depends on having a pre-existing notion of intensional identity type. Hofmann used Martin-Löf’s notion, the indexed family inductively generated from proofs of reflexivity [B. Nordström et al., 1990]. The recent homotopical view of identity in terms of path types [The Univalent Foundations Program, 2013] gives a more liberal perspective and has brought with it the notion of higher inductive type (HIT) [P. L. Lumsdaine and M. Shulman, 2019], subsuming both inductive and quotient types. Inductively defined indexed families of types (in all their various forms) are perhaps the most useful concept that dependent type theory has contributed to the practice of computer assistance for formalizing mathematical proofs. However, it is often the case that a particular application of such types needs not only to inductively generate a collection of objects, but also to make identifications between the objects. In classical mathematics one can first generate and then identify, using the Axiom of Choice to lift infinitary constructions to the quotient. HITs can allow one to avoid such non-constructive uses of choice by inter-twining generation and identification. Perhaps more important than the constructive/non-constructive issue is that simultaneously declaring how to generate and how to identify can be a very natural way of defining some construct from the user’s point of view. This is why HITs promise to be so useful, once we have robust and convenient mechanisms in theorem-proving systems for defining HITs and defining functions out of HITs. Although some HITs have been axiomatized in various systems, at the moment the only system I know of with built in support for defining quite general forms of HIT and using them is the implementation of cubical type theory [C. Cohen et al., 2018] within recent versions of the Agda system [A. Vezzosi et al., 2019]. The higher dimensional aspect of identity in cubical type theory is fascinating; nevertheless, the simpler one-dimensional version of identity, in which one has uniqueness of identity proofs (UIP), is adequate for many applications. Although some regard UIP as a bug of early versions of Agda with it’s original form of dependent pattern matching [T. Coquand, 1992], it is by choice a feature of the Lean prover [J. Avigad et al., 2020]. Altenkirch and Kaposi [T. Altenkirch and A. Kaposi, 2016] have termed the one-dimensional version of HITs quotient inductive types (QITs) and they promise to be very useful even in the setting of type theory with UIP. In this talk I survey some of these developments, including a recent reduction of QITs to quotients [M. P. Fiore et al., 2020], and the prospects for better support in theorem-provers for quotient constructions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
Keywords
  • dependent type theory
  • quotient
  • quotient inductive type
  • theorem-proving systems

Metrics

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

References

  1. T. Altenkirch and A. Kaposi. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16, pages 18-29, New York, NY, USA, 2016. ACM. Google Scholar
  2. J. Avigad, L. de Moura, and S. Kong. Theorem Proving in Lean, 3.4.0 edition, February 2020. Google Scholar
  3. C. Cohen, T. Coquand, S. Huber, and A. Mörtberg. Cubical type theory: A constructive interpretation of the univalence axiom. In T. Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  4. R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Inc., USA, 1986. Google Scholar
  5. T. Coquand. Pattern matching with dependent types. In B. Nordström, K. Petersson, and G. D. Plotkin, editors, Proceedings of the 1992 Workshop on Types for Proofs and Programs, Båstad, Sweden, pages 66-79, June 1992. Google Scholar
  6. M. P. Fiore, A. M. Pitts, and S. C. Steenkamp. Constructing infinitary quotient-inductive types. In J. Goubault-Larrecq and B. König, editors, 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2020), volume 12077 of Lecture Notes in Computer Science, pages 257-276. Springer, 2020. Google Scholar
  7. M. Hofmann. Extensional Concepts in Intensional Type Theory. PhD thesis, University of Edinburgh, 1995. Google Scholar
  8. P. L. Lumsdaine and M. Shulman. Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society, page 1–50, 2019. Google Scholar
  9. B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf’s Type Theory. Oxford University Press, 1990. Google Scholar
  10. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations for Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013. URL: http://homotopytypetheory.org/book.
  11. A. Vezzosi, A. Mörtberg, and A. Abel. Cubical agda: A dependently typed programming language with univalence and higher inductive types. Proc. ACM Program. Lang., 3(ICFP):87:1-87:29, July 2019. 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