## Stream: new members

### Topic: Why are quotient types not inductive types?

#### Chris M (Jul 28 2020 at 05:20):

From Theorem proving in Lean, quotient types are defined as:

universes u v

constant quot : Π {α : Sort u}, (α → α → Prop) → Sort u

constant quot.mk :
Π {α : Sort u} (r : α → α → Prop), α → quot r

axiom quot.ind :
∀ {α : Sort u} {r : α → α → Prop} {β : quot r → Prop},
(∀ a, β (quot.mk r a)) → ∀ (q : quot r), β q

constant quot.lift :
Π {α : Sort u} {r : α → α → Prop} {β : Sort u} (f : α → β),
(∀ a b, r a b → f a = f b) → quot r → β


Why are quot and quot.mk introduced as constants ? Why not use inductive or structurefor quot with a constructor mk?

#### Scott Morrison (Jul 28 2020 at 05:21):

Because there'd be no way to get equality to work the way you expect on quotient types.

#### Scott Morrison (Jul 28 2020 at 05:22):

This is one of the lovely things about Lean. Coq doesn't provide axiomatic quotient types, and they have to live in "setoid hell" instead, carrying around a non-equality equivalence relation when talking about quotients.

#### Chris M (Jul 28 2020 at 05:24):

Why is equality so much better than \iff? I've heard this a lot (also in favor of univalent foundation).

#### Yury G. Kudryashov (Jul 28 2020 at 05:51):

Because you can rewrite on a = b without verifying Proper (in terms of coq).

#### Utensil Song (Jul 28 2020 at 06:37):

For this question, you might want to read 2.7.1 Quotient types, 3.8 Differences from Coq (particularly 7 & 8) and 4.1 The $\kappa$ reduction (look for $\iota_q$) in https://github.com/digama0/lean-type-theory/tree/v1.0 .

If I'm reading it correctly, to make quotient types work in Lean, you need these constants and the one axiom in pure Lean, plus one computational rule ($\iota_q$) in Lean kernel which doesn't exist in Coq. And Lean doesn't support adding computational rules to the kernel from pure Lean so it can't be mimicked by inductive etc.

#### Eric Wieser (Jul 28 2020 at 06:46):

@Scott Morrison: carrying around a setoid (admittedly behind a type class) is exactly what quotient (not quot) does though, right?

#### Utensil Song (Jul 28 2020 at 07:04):

The computational rule is implemented in C++, quotient_normalizer_extension::operator() in Lean 3 and quot_reduce_rec in Lean 4.

#### Utensil Song (Jul 28 2020 at 07:05):

(I looked for the C++ code in Lean 4 because I was remotely hoping it's moved to pure Lean but no)

#### Mario Carneiro (Jul 28 2020 at 08:25):

Actually, I was talking about this with Jeremy yesterday, and I don't think that we really need the quotient computation rule. We could probably get away with a propositional version of quot.beta without too much pain, because we still have proof irrelevance to smooth over the sharp edges of setoid hell. And if you have a non-computational quotient type, then you don't even need to axiomatize it - the usual construction of set quotients works without any extra axioms. (I think the proof of funext breaks though, so you would have to add that as an axiom.)

#### Reid Barton (Jul 28 2020 at 12:15):

From what I understand you can also replicate Lean's quotient types in Coq using unsafe features--but it's unsafe only because it happens outside the kernel; otherwise the same thing is happening as in Lean.

Last updated: May 07 2021 at 00:30 UTC