Quotient types and proof irrelevance

Stream: general

[suhr]

Do I understand it correctly that quotient types in Lean require proof irrelevance of Prop? Specifically, this seems to follow from this proof in Core.lean:

theorem exists_rep {α : Sort u} {r : α → α → Prop} (q : Quot r) : Exists (fun a => (Quot.mk r a) = q) :=
  q.inductionOn (fun a => ⟨a, rfl⟩)

[Mario Carneiro]

No, quotient types do not directly rely on proof irrelevance, although it is possible that the statement of inductionOn requires it because the generalized version of that statement only works on subsingletons (otherwise you have to use Quot.lift and prove that the choice you made is coherent with the relation).

[Mario Carneiro]

The lean 2 HoTT implementation of quotient types did not have proof irrelevance

[Mario Carneiro]

But at this point proof irrelevance is baked fairly deeply into the way lean 4 works, so it's a difficult counterfactual to consider today. Things that casually assume proof irrelevance are all over the place

[suhr]

So, Quot.ind might depend on proof irrelevance, but generally you can use Quot.lift instead of Quot.lift? Is it possible to prove Quot.ind from Quot.lift?

But at this point proof irrelevance is baked fairly deeply into the way lean 4 works, so it's a difficult counterfactual to consider today. Things that casually assume proof irrelevance are all over the place

Sure. I just try to explain both quotients and proof irrelevance in a tutorial, so I need to know how things depend on each other.

[Mario Carneiro]

you might need the dependent version of Quot.lift

[Mario Carneiro]

I think Quot.recOn exists

[Mario Carneiro]

Quotient types without proof irrelevance behave rather differently to set-quotients, you would use different axioms to introduce them

[Mario Carneiro]

For the purpose of a tutorial, I would just introduce proof irrelevance first

[suhr]

And Quot.recOn is implemented using Quot.ind. So I guess it really has proof irrelevance baked in.

Anyway, thanks. I will probably indeed introduce proof irrelevance first.

[Mario Carneiro]

Quot.recOn could be an axiom and Quot.ind defined in terms of it; the current ordering is preferred because it is simpler

[Mario Carneiro]

Quot.ind does not depend on proof irrelevance (it doesn't make sense to say an axiom depends on another axiom), it is just a weird axiom otherwise

[Mario Carneiro]

you can't use Quot.ind or indeed any axiom to prove proof irrelevance because it is a definitional equality. The best you can hope for is proving propositional proof irrelevance from Quot.ind

[suhr]

Well, I use “proof irrelevance” somewhat loosely, including the rejection of large elimination for types in Prop.

[Mario Carneiro]

well quotients are definitely not small eliminators

[Mario Carneiro]

that's what Quot.lift / Quot.recOn is about