# Zulip Chat Archive

## Stream: general

### Topic: why is quot an axiom?

#### Kevin Buzzard (Dec 21 2018 at 22:33):

Can't we just do it like this?

import tactic.interactive -- Lean has the "quotient" function to make equivalence classes. -- Here I try to figure out why it is needed. universes u v namespace xena -- this doesn't work with Prop but do I care? variable {β : Type u} variable (r : β → β → Prop) -- equiv reln closure of r inductive requiv {β : Type u} (r : β → β → Prop) : β → β → Prop | of_r (a b : β) : r a b → requiv a b | refl (a : β) : requiv a a | symm ⦃a b : β⦄ : requiv a b → requiv b a | trans ⦃a b c : β⦄ : requiv a b → requiv b c → requiv a c definition equiv_class (r : β → β → Prop) (b : β) : set β := {c : β | requiv r b c} definition quot {β : Type u} (r : β → β → Prop) : Type u := {eq_cl : set β // ∃ a : β, equiv_class r a = eq_cl} namespace quot definition mk : Π {α : Type u} (r : α → α → Prop), α → quot r := λ α r a, ⟨equiv_class r a,a,rfl⟩ theorem ind : ∀ {α : Type u} {r : α → α → Prop} {β : quot r → Prop}, (∀ (a : α), β (mk r a)) → ∀ (q : quot r), β q := λ α r β h q, begin rcases q with ⟨C,a,Ha⟩, convert h a, rw Ha, end noncomputable definition lift : Π {α : Type u} {r : α → α → Prop} {β : Sort v} (f : α → β), (∀ (a b : α), r a b → f a = f b) → quot r → β := λ α r β f h q,begin apply f, rcases q with ⟨C,HC⟩, -- cases HC with a Ha, MEH let a := classical.some HC, have Ha : equiv_class r a = C := classical.some_spec HC, -- ask about better way exact a, end definition sound : ∀ {α : Type u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b := λ α r a b h,begin unfold mk, suffices : equiv_class r a = equiv_class r b, simp [this], ext, split, { intro Hx, show requiv r b x, apply requiv.trans _ Hx, apply requiv.symm, apply requiv.of_r, assumption, }, { intro Hx, show requiv r a x, apply requiv.trans _ Hx, apply requiv.of_r, assumption, } end end quot end xena

I think I do all the basic theory of `quot`

. I've been teaching quotients (in ZFC) in my class and I was trying to figure out how to explain to mathematicians why all this `quot.sound`

stuff all had to be dealt with via extra axioms, but I've just done it all myself. The two sacrifices I had to make were: (1) it doesn't work for props (but who takes a quotient on proofs of a prop?) and (2) `lift`

(the map which mathematicians think of as a "descent", quite the other direction to the computer science word) is noncomputable. What does `quot.sound`

offer that my set-up doesn't but which I want or need?

#### Kevin Buzzard (Dec 21 2018 at 22:33):

I just make the quotient type as a bunch of equivalence classes.

#### Kevin Buzzard (Dec 21 2018 at 22:34):

A subtype of `set β`

consisting of the equiv classes.

#### Reid Barton (Dec 21 2018 at 22:40):

The differences are that `lift`

is computable, and `lift f _ (mk r x) = f x`

(which it looks like you haven't proved, but I'm sure you can) hold definitionally (this is `quot.lift_beta`

).

#### Kevin Buzzard (Dec 21 2018 at 23:01):

Actually I'm struggling with the theorem about lift:

-- the computation principle variables (β : Type v) (f : α → β) (a : α) variable (h : ∀ a b , r a b → f a = f b) theorem thm : lift f h (mk r a) = f a := begin rcases (mk r a) with ⟨C,HC⟩, -- HC has nothing to do with a now. let b := classical.some HC, have Hb : equiv_class r b = C := classical.some_spec HC, /- α : Type u, r : α → α → Prop, β : Type v, f : α → β, a : α, h : ∀ (a b : α), r a b → f a = f b, C : set α, HC : ∃ (a : α), equiv_class r a = C, b : α := classical.some HC, Hb : equiv_class r b = C ⊢ lift f h ⟨C, HC⟩ = f a -/ show f b = f a, apply h b a, -- but I don't know a ∈ C sorry end

#### Chris Hughes (Dec 22 2018 at 00:14):

Also, your proof of `sound`

uses `quot.sound`

#### Kevin Buzzard (Dec 22 2018 at 11:57):

Oh does it? I suppose that's cheating :-)

#### Mario Carneiro (Dec 22 2018 at 12:25):

You use set extensionality in the proof, which is an axiom in ZFC and is derived from `propext`

and `quot.sound`

in lean

#### Kevin Buzzard (Dec 24 2018 at 09:35):

OK so I proved `xena.quot.thm`

. I think definitional equality is overrated, and if I have my maths hat on I'd say the same about computability. I am concerned about Chris' comment though. I am doing this to try and figure out how to explain to mathematicians why Lean wants quotients to be an extra axiom. But set extensionality is implied by function extensionality, right? Would another approach have been to make funext and/or propext axioms and then get quotients using my method? At least if we decide not to care about computability and definitional equality and be 100% mathematician.

#### Mario Carneiro (Dec 24 2018 at 09:53):

yes, that's called zfc

#### Mario Carneiro (Dec 24 2018 at 09:53):

you make set.ext an axiom

#### Mario Carneiro (Dec 24 2018 at 09:53):

and derive funext and the others by constructing everything from sets

#### Mario Carneiro (Dec 24 2018 at 09:54):

if you want to convince yourself, make a copy of `set.ext`

as an actual axiom, and then derive all that and check that you didn't use propext or quot.sound in `#print axioms`

#### Kevin Buzzard (Feb 15 2019 at 23:58):

I now understand this quotient stuff better. I always understand stuff better with an example, and whilst equivalence classes of continuous non-archimedean valuations on a topological ring might not be the example best suited to everyone, working a lot on this example now I'm back on the perfectoid project has made me see the big picture much better.

Here's something I don't understand going back to the conversation above though. I can see why `lift f _ (mk r x) = f x`

isn't going to be proved by `rfl`

in my set-up above (quotients as equivalence classes), but now I don't understand why it can be proved with `rfl`

if we use Lean's inbuilt quotient. If TPIL is to believed, the whole `quot`

set-up in core is just made by writing down a load of axioms. How can `rfl`

prove the computation law for `quot`

?

#### Mario Carneiro (Feb 16 2019 at 00:00):

because it's an axiom

#### Mario Carneiro (Feb 16 2019 at 00:00):

it's literally baked into lean that this happens

#### Kevin Buzzard (Feb 16 2019 at 00:01):

I don't see the axiom in TPIL

#### Mario Carneiro (Feb 16 2019 at 00:01):

that's why `quot`

has special magic powers you can't achieve even with isomorphic constructions

#### Kevin Buzzard (Feb 16 2019 at 00:01):

but this gives me an idea -- why don't I make the computation law I want to be true by `rfl`

an axiom?

#### Kevin Buzzard (Feb 16 2019 at 00:02):

I can prove it after all, so it's true, so it's safe to make it an axiom, and then I can prove it with `rfl`

?

#### Mario Carneiro (Feb 16 2019 at 00:02):

not necessarily

#### Mario Carneiro (Feb 16 2019 at 00:02):

just because it's true doesn't mean it's a good reduction rule - you've seen that with `simp`

#### Mario Carneiro (Feb 16 2019 at 00:03):

and I mean axiom in the conventional sense of "a thing that lets you prove things you couldn't before", not the lean sense of "a constant with no computation rules that is called `axiom`

or `constant`

"

#### Kevin Buzzard (Feb 16 2019 at 00:03):

Oh. You mean "it's in the C++ code"?

#### Mario Carneiro (Feb 16 2019 at 00:03):

basically

#### Mario Carneiro (Feb 16 2019 at 00:05):

one of the things I want to experiment with in the fork is user computation rules, which would allow you to install your own computation rules just like you can add your own axioms

#### Johan Commelin (Feb 16 2019 at 05:10):

@Mario Carneiro But in our case of a "fake" quotient, I guess it would be a *good reduction rule*. Is that true?

#### Mario Carneiro (Feb 16 2019 at 07:26):

It's hard to say. Part of the problem with having computation rules on a type that's not a constant (like `quot`

) is that there are *already* computation rules, if not very useful ones, and adding a reduction rule on top of that can cause failure of confluence

#### Mario Carneiro (Feb 16 2019 at 07:27):

For a structure, that will be things like a projection on a structure instance computing to the value

Last updated: May 08 2021 at 17:33 UTC