{"@context":"https:\/\/schema.org\/","@type":"ScholarlyArticle","@id":"#article13755","name":"Quotients in Dependent Type Theory (Invited Talk)","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\u00f6f\u2019s notion, the indexed family inductively generated from proofs of reflexivity [B. Nordstr\u00f6m 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.\r\nInductively 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\u2019s 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].\r\nThe 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\u2019s 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.\r\nIn 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.","keywords":["dependent type theory","quotient","quotient inductive type","theorem-proving systems"],"author":{"@type":"Person","name":"Pitts, Andrew M.","givenName":"Andrew M.","familyName":"Pitts","sameAs":"https:\/\/orcid.org\/0000-0001-7775-3471","affiliation":"Department of Computer Science & Technology, University of Cambridge, UK"},"position":3,"pageStart":"3:1","pageEnd":"3:2","dateCreated":"2020-06-28","datePublished":"2020-06-28","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/3.0\/legalcode","copyrightHolder":{"@type":"Person","name":"Pitts, Andrew M.","givenName":"Andrew M.","familyName":"Pitts","sameAs":"https:\/\/orcid.org\/0000-0001-7775-3471","affiliation":"Department of Computer Science & Technology, University of Cambridge, UK"},"copyrightYear":"2020","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2020.3","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","citation":"http:\/\/homotopytypetheory.org\/book","isPartOf":{"@type":"PublicationVolume","@id":"#volume6370","volumeNumber":167,"name":"5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)","dateCreated":"2020-06-28","datePublished":"2020-06-28","editor":{"@type":"Person","name":"Ariola, Zena M.","givenName":"Zena M.","familyName":"Ariola","email":"mailto:ariola@cs.uoregon.edu","affiliation":"University of Oregon, Eugene, Oregon, USA"},"isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#article13755","isPartOf":{"@type":"Periodical","@id":"#series116","name":"Leibniz International Proceedings in Informatics","issn":"1868-8969","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#volume6370"}}}