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