## Stream: general

### Topic: Quotient types and proof irrelevance

#### suhr (Nov 18 2022 at 17:47):

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 (Nov 18 2022 at 19:32):

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 (Nov 18 2022 at 19:33):

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

#### Mario Carneiro (Nov 18 2022 at 19:34):

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 (Nov 18 2022 at 19:49):

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 (Nov 18 2022 at 19:50):

you might need the dependent version of Quot.lift

#### Mario Carneiro (Nov 18 2022 at 19:50):

I think Quot.recOn exists

#### Mario Carneiro (Nov 18 2022 at 19:52):

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

#### Mario Carneiro (Nov 18 2022 at 19:54):

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

#### suhr (Nov 18 2022 at 19:58):

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 (Nov 18 2022 at 20:04):

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 (Nov 18 2022 at 20:05):

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 (Nov 18 2022 at 20:07):

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 (Nov 18 2022 at 20:10):

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

#### Mario Carneiro (Nov 18 2022 at 20:12):

well quotients are definitely not small eliminators

#### Mario Carneiro (Nov 18 2022 at 20:12):

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

Last updated: Dec 20 2023 at 11:08 UTC