Why are quotient types not inductive types?

Stream: new members

[Chris M]

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]

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

[Scott Morrison]

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]

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

[Yury G. Kudryashov]

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

[Utensil Song]

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]

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

[Utensil Song]

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

[Utensil Song]

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

[Mario Carneiro]

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]

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.