Quotient types

Plain-language version: What the axioms are

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

A quotient type is a type whose elements are those of an existing type, with every pair related by a given relation made equal. Mathematics constructs such objects constantly: the integers modulo $n$, rational numbers as fractions up to cancellation, finite sets as lists up to order and repetition. Lean provides quotients as a primitive of its type theory: four constants, one axiom and one computation rule. This page sets out those rules, the Setoid and Quotient layer built on them, a worked example, and what the computation rule buys.

The primitives

The constants are introduced early in Lean's core library by a dedicated command, init_quot, not by an inductive definition. Lean prints them so:

#print Quot
#check @Quot.mk
#check @Quot.lift
#check @Quot.ind
#check @Quot.sound

Quotient primitive Quot.{u} : {α : Sort u} → (α → α → Prop) → Sort u
@Quot.mk : {α : Sort u_1} → (r : α → α → Prop) → α → Quot r
@Quot.lift : {α : Sort u_1} →
  {r : α → α → Prop} → {β : Sort u_2} → (f : α → β) → (∀ (a b : α), r a b → f a = f b) → Quot r → β
@Quot.ind : ∀ {α : Sort u_1} {r : α → α → Prop} {β : Quot r → Prop}, (∀ (a : α), β (Quot.mk r a)) → ∀ (q : Quot r), β q
@Quot.sound : ∀ {α : Sort u_1} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b

As rules: for any relation $r$ on $A$ there is a type, and every element of $A$ gives an element of it,

$\frac{\Gamma ⊢A:\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}u\Gamma ⊢r:A\to A\to \mathrm{P}\mathrm{r}\mathrm{o}\mathrm{p}}{\Gamma ⊢\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}r:\mathrm{S}\mathrm{o}\mathrm{r}\mathrm{t}u}\frac{\Gamma ⊢a:A}{\Gamma ⊢\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}\mathrm{.}\mathrm{m}\mathrm{k}ra:\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}r}$

A function out of the quotient is a function out of $A$ together with a proof that it respects $r$:

$\frac{\Gamma ⊢f:A\to B\Gamma ⊢h:\Pi (ab:A).rab\to fa=fb}{\Gamma ⊢\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}\mathrm{.}\mathrm{l}\mathrm{i}\mathrm{f}\mathrm{t}fh:\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}r\to B}$

and it computes on representatives:

$\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}\mathrm{.}\mathrm{l}\mathrm{i}\mathrm{f}\mathrm{t}fh(\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}\mathrm{.}\mathrm{m}\mathrm{k}ra)\equiv fa$

The induction principle Quot.ind says that, for proving a proposition, every element may be taken to be some Quot.mk r a. Finally the axiom identifies related representatives:

$\frac{\Gamma ⊢p:rab}{\Gamma ⊢\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}\mathrm{.}\mathrm{s}\mathrm{o}\mathrm{u}\mathrm{n}\mathrm{d}p:\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}\mathrm{.}\mathrm{m}\mathrm{k}ra=\mathrm{Q}\mathrm{u}\mathrm{o}\mathrm{t}\mathrm{.}\mathrm{m}\mathrm{k}rb}$

Only Quot.sound is an axiom in any real sense. Carneiro observes that Quot, Quot.mk, Quot.lift and the computation rule are all satisfied by reading the quotient as $A$ itself, Quot.mk as the identity and Quot.lift f h as f; Theorem Proving in Lean 4 notes that Quot.ind holds under the same reading. What that reading cannot satisfy is the identification of distinct representatives. Because the computation rule is a reduction and not a constant, Carneiro calls quotients a semi-built-in feature: Lean's kernel has to know about them, and they are switched on as a whole.

The relation need not be an equivalence relation. The rules for Quot and Eq together make equality in Quot r the equivalence relation generated by $r$.

An example: unordered pairs

An unordered pair is an ordered pair taken up to swapping its components. The relation below holds when one pair is the other reversed. It is symmetric but not reflexive, and Quot does not mind.

/-- `p` and `q` are related when `q` is `p` with its components swapped. -/
def Swapped (α : Type) (p q : α × α) : Prop := p.1 = q.2 ∧ p.2 = q.1

def UPair (α : Type) : Type := Quot (Swapped α)

def UPair.mk {α : Type} (a b : α) : UPair α := Quot.mk (Swapped α) (a, b)

theorem UPair.mk_comm {α : Type} (a b : α) : UPair.mk a b = UPair.mk b a :=
  Quot.sound ⟨rfl, rfl⟩

def UPair.sum (u : UPair Nat) : Nat :=
  Quot.lift (fun p => p.1 + p.2)
    (fun p q (h : Swapped Nat p q) => by rw [h.1, h.2, Nat.add_comm])
    u

example : UPair.sum (UPair.mk 3 4) = 7 := rfl
#eval UPair.sum (UPair.mk 3 4)

theorem UPair.sum_pos (u : UPair Nat) (h : ∀ a b, UPair.mk a b = u → 0 < a) :
    0 < UPair.sum u := by
  induction u using Quot.ind with
  | mk p => exact Nat.lt_of_lt_of_le (h p.1 p.2 rfl) (Nat.le_add_right _ _)

#print axioms UPair.mk_comm
#print axioms UPair.sum
#print axioms UPair.sum_pos

7
'UPair.mk_comm' depends on axioms: [Quot.sound]
'UPair.sum' does not depend on any axioms
'UPair.sum_pos' does not depend on any axioms

Each primitive has its part. UPair.mk_comm is the one statement that needs the axiom: it asserts that two different representatives give the same element. The sum is defined by Quot.lift, and the obligation it carries is the proof that swapping the components does not change p.1 + p.2. A function that does not respect the relation, such as the first component, cannot be lifted, because no such proof exists. The example is closed by rfl: the computation rule reduces UPair.sum (UPair.mk 3 4) to 3 + 4, and then to 7. The theorem UPair.sum_pos uses Quot.ind to reduce a statement about every unordered pair to one about representatives. Neither the definition nor the induction uses an axiom; only the identification of representatives does.

Setoid and Quotient

When the relation is an equivalence relation, the core library bundles it as a setoid: a type with a chosen relation and a proof that it is reflexive, symmetric and transitive. Quotient s is then Quot applied to the setoid's relation.

#print Setoid
#print Quotient

instance parity : Setoid Nat where
  r a b := a % 2 = b % 2
  iseqv := ⟨fun _ => rfl, fun h => h.symm, fun h₁ h₂ => h₁.trans h₂⟩

def Mod2 : Type := Quotient parity

def Mod2.ofNat (n : Nat) : Mod2 := Quotient.mk parity n

def Mod2.isOdd : Mod2 → Bool :=
  Quotient.lift (fun n => n % 2 == 1) (fun a b (h : a % 2 = b % 2) => by rw [h])

example : Mod2.ofNat 3 = Mod2.ofNat 7 := Quotient.sound rfl
example : Mod2.isOdd (Mod2.ofNat 7) = true := rfl

theorem Mod2.two_ne_three : Mod2.ofNat 2 ≠ Mod2.ofNat 3 := fun h =>
  absurd (show 2 % 2 = 3 % 2 from Quotient.exact h) (by decide)

#print axioms Mod2.two_ne_three

class Setoid.{u} (α : Sort u) : Sort (max 1 u)
number of parameters: 1
fields:
  Setoid.r : α → α → Prop
  Setoid.iseqv : Equivalence Setoid.r
constructor:
  Setoid.mk.{u} {α : Sort u} (r : α → α → Prop) (iseqv : Equivalence r) : Setoid α
def Quotient.{u} : {α : Sort u} → Setoid α → Sort u :=
fun {α} s => Quot Setoid.r
'Mod2.two_ne_three' depends on axioms: [propext]

Mod2 is the integers modulo 2, built from the natural numbers. Showing that 3 and 7 have the same class is Quotient.sound applied to a proof that 3 % 2 = 7 % 2, which holds by computation. Showing that 2 and 3 have different classes needs the converse, that equal classes come from related representatives. That is Quotient.exact, and it is where the equivalence relation matters. Its proof lifts the relation itself to a proposition-valued function on pairs of classes; the obligation is that related inputs give equal propositions, which needs propositional extensionality, and reflexivity then closes the argument. The output records it: the proof that two classes differ depends on propext, not on Quot.sound.

What the computation rule buys

Because Quot.lift reduces on Quot.mk, a function defined on a quotient computes. rfl proves UPair.sum (UPair.mk 3 4) = 7, and #eval runs the same function. The reference manual contrasts this with working directly on sets of equivalence classes: functions out of such sets need non-computational classical principles, whereas functions out of a quotient are ordinary functions that also respect a relation. It also notes that the quotient leaves definitional equality untouched: two elements of a quotient are definitionally equal exactly when their representatives are. Elements made equal by Quot.sound are equal propositionally, by a proof.

The rule is also what makes function extensionality a theorem. Quotienting a function type by pointwise equality and applying each class to an argument reduces, by this rule, back to the original function. A propositional version of the rule would not do, because using it under a binder would already need function extensionality. Theorem Proving in Lean 4 likewise presents function extensionality as a consequence of the quotient construction.

The compiler erases Quot.lift. The core library carries an unsafe constant, Quot.lcInv, documented as the device for doing so, and the reference manual notes that Squash α, the quotient of α by the relation that relates everything, is represented at run time exactly as α is.

Limits

Quot is not an inductive type. In consequence, a recursive occurrence of the type being defined may not appear inside a quotient in an inductive definition, as it may inside a List:

inductive SetTree (α : Type u) where
  | leaf : α → SetTree α
  | branch : Quot (fun (xs ys : List (SetTree α)) => True) → SetTree α

Lean rejects it with (kernel) arg #2 of 'SetTree.branch' contains a non valid occurrence of the datatypes being declared. The reference manual's remedy is to define the type without the nested quotient and then quotient the whole type by a relation that identifies the intended trees.

Quotients are also one of the places where the checker's algorithm and the type theory part company. Carneiro shows that a quotient of a proposition behaves like a subsingleton eliminator, and with it gives an instance where the checker's definitional-equality test is not transitive. The page on proof irrelevance and subsingleton elimination treats the main case of this, which comes from the accessibility predicate.

Other proof assistants make different choices. Carneiro noted in 2019 that Coq had no quotient types with a computation rule, so that its users worked with setoids, types paired with an equivalence relation that stands in for equality.

Next

The three axioms places Quot.sound beside propext and Classical.choice.