© Andrew M. Pitts; licensed under Creative Commons License CC-BY 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). 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 [4] for extensional type theory. Later Hofmann formulated a version for intensional type theory in his thesis [7]. 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 [9, chapter 8]. The recent homotopical view of identity in terms of path types [10] gives a more liberal perspective and has brought with it the notion of higher inductive type (HIT) [8], 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 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 [3] within recent versions of the Agda system [11]. 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 [5], it is by choice a feature of the Lean prover [2]. Altenkirch and Kaposi [1] 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 [6], and the prospects for better support in theorem-provers for quotient constructions.