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 theoremproving 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 preexisting notion of intensional identity type. Hofmann used MartinLö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 nonconstructive uses of choice by intertwining generation and identification. Perhaps more important than the constructive/nonconstructive 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 theoremproving 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 onedimensional 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 onedimensional 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 theoremprovers for quotient constructions.
BibTeX  Entry
@InProceedings{pitts:LIPIcs:2020:12325,
author = {Andrew M. Pitts},
title = {{Quotients in Dependent Type Theory (Invited Talk)}},
booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
pages = {3:13:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771559},
ISSN = {18688969},
year = {2020},
volume = {167},
editor = {Zena M. Ariola},
publisher = {Schloss DagstuhlLeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12325},
URN = {urn:nbn:de:0030drops123256},
doi = {10.4230/LIPIcs.FSCD.2020.3},
annote = {Keywords: dependent type theory, quotient, quotient inductive type, theoremproving systems}
}
Keywords: 

dependent type theory, quotient, quotient inductive type, theoremproving systems 
Collection: 

5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) 
Issue Date: 

2020 
Date of publication: 

28.06.2020 