# Zulip Chat Archive

## 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: Aug 03 2023 at 10:10 UTC