Quotient axioms

Stream: general

[Patrick Johnson]

While I was reading TPIL, I was wondering why do we need the quotient axioms (quot, quot.mk, quot.ind, quot.lift and quot.sound)? I mean, why do they need to be stated as constants and axioms, rather than definitions and lemmas? If r is an equivalence relation, all of them can be implemented using the axiom of choice. If it is not, what is the purpose of using quotients in that case? Is there some data structure or mathematical object that can't be represented without them?

[Eric Wieser]

Is docs#quot.ind a constant? I thought it was implemented in terms of something else

[Eric Wieser]

https://github.com/leanprover-community/lean/blob/e948149d3d1bbdb8eac9cd103d58626a59fae3b9/library/init/core.lean#L92 has some context you may have already found, but I'm not sure I believe the comment.

[Kyle Miller]

@Eric Wieser quot.ind is a constant.

#print quot.ind
/-
builtin-quotient-type-constant quot.ind : ∀ {α : Sort u} {r : α → α → Prop} {β : quot r → Prop},
  (∀ (a : α), β (quot.mk r a)) → ∀ (q : quot r), β q
-/

[Reid Barton]

@Patrick Johnson I assume you mean using something like equivalence classes to implement quot. If you do that then you can indeed define these constants, but you won't have the computation rule for applying quot.lift to quot.mk as a definitional equality.

[Kyle Miller]

@Patrick Johnson My understanding is that they're designed to give you quotients in a computable way. They're also used to prove docs#funext

I think an idea here is that part of an interface of a Type is its associated eq relation. The quot system is a way to let you say "and now these terms are eq, too" while making sure that whenever you look at underlying terms you do so in a way that provably respects this new eq.

[Kevin Buzzard]

Yeah you can (indeed I did when I was trying to understand this) reimplement quotients using equivalence classes. You have to restrict to type rather than sort and you lose that the proof of the fundamental commuting diagram is refl

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

Quotients a la Lean makes lean's type theory have some properties which some people find undesirable but which don't seem to bother mathematicians

[Patrick Johnson]

Thanks. So, to summarize, if I got it right, the quotient axioms exist in Lean only for pragmatic purposes, and not for the foundational purposes? It means they are not needed for the underlying logic framework, but just to facilitate defeq-related stuff.

[Patrick Johnson]

You have to restrict to type rather than sort...

Are you sure about that?

[Kyle Miller]

Patrick Johnson said:

and not for the foundational purposes?

(I believe that's with the proviso that you'd need to include funext as an axiom instead.)

[Kevin Buzzard]

Re type not sort, I'm just going from memory. I guess I can reconstruct what happened: an equivalence class for an equivalence relation is a subset but IIRC lean doesn't let you make subsets of P : Prop.

[Kevin Buzzard]

docs#set docs#quotient

[Kevin Buzzard]

Yeah quotient allows sorts but set only allows types

[Mario Carneiro]

That quotient allows Sort u (and in particular, produces a Prop when the input is a Prop, rather than having type Sort (max 1 u) like stuff built with inductive types) is arguably a bug, and it leads to one of the two examples of non-transitivity of defeq, mentioned in section 3.1.1 of #leantt