# Zulip Chat Archive

## 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 `structure`

for `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