General results about set quotients

[cangiuli]

This PR adds several general-purpose lemmas about set quotients:

• HoTT Book Lemma 6.10.8: If we have a function r sending each element of A to its "canonical representative" under the relation R, then the set of fixed points of r (i.e., the set of canonical representatives) satisfies the universal property of the quotient A/R and is equivalent to it.
• (added in 14019af) If p : A -> B is a surjection into a set, then B is the quotient of A by x ~ y := p x = p y.
• HoTT Book Corollary 6.10.10: If p : A -> B is a retraction into a set, then B is the quotient of A by x ~ y := p x = p y.
• Every set A is equivalent to A / _≡_.

If you can think of any better names for these results, please let me know. :)

[anshwad10]

About quotRetractEquiv: Doesn't it suffice for p to be a surjection, not necessarily a retraction?

[cangiuli]

@anshwad10 Yes, good point!

I'll note that the statement I formalized is already stronger than what's in the HoTT Book in that it doesn't require isSet A, since it doesn't go through equivQuotCR (Lemma 6.10.8). (Actually, I tried going through that result, but the proof was quite a bit longer than the current "direct" one, because a bunch of the details are fiddly.)

I'm not sure whether I should actually add the even stronger statement that isSurjection p suffices to this PR, because the proof is more complicated (since we need to fiddle with truncations) and I don't have a use case in mind at the moment...

[mortberg]

Good stuff! I would be happy to merge as is and you can add the suggested result in a future PR, or you can do it now. Let me know what you want me to do

[cangiuli]

OK, I found an even cleaner way to prove the more general result that @anshwad10 suggested (when p is a surjection), and I now derive the previous result (when p is a retraction) from it. I'm happy for you to merge this as soon as you approve.

[mortberg]

Very nice!