# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeFeb 19th 2016
• (edited Feb 19th 2016)

I notice that there seemed to be no-where a really explicit semantics explanation of the claim that “univalence implies the existence of quotient types”. I checked with Peter Lumsdaine, and he kindly provided some text which, up to some minor reformatting, I have put into quotient type – Properties – from univalence.

• CommentRowNumber2.
• CommentAuthorDavid_Corfield
• CommentTimeMar 29th 2016

What does ’u.m.p.’ mean in

(For the subobject classification u.m.p…. ?

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeMar 29th 2016

I forget, but the lead-in of the sentence just means to say “To see how the axioms for a subobject classifier are satisfied: ….”. I have edited accordingly.

• CommentRowNumber4.
• CommentAuthorZhen Lin
• CommentTimeMar 29th 2016

“Universal mapping property”, I believe.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeMar 29th 2016
• (edited Mar 29th 2016)

That must be it.

If anyone feels energetic, it would be great if there were more on the nLab on the classical construction of quotients from subobject classifiers. Such, or pointer to such, is presently missing at elementary topos and quotient object etc.

• CommentRowNumber6.
• CommentAuthorTodd_Trimble
• CommentTimeMar 29th 2016

I’ve been meaning to complete and release some notes on the “down-to-earth” way to construct colimits in a topos, including quotients. At some point I can add a description to quotient object. Of course there is also the argument due to Paré.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeMar 29th 2016
• (edited Mar 29th 2016)

That would be great if you could add something.

What’s the precise citation to Paré?

• CommentRowNumber8.
• CommentAuthorTodd_Trimble
• CommentTimeMar 29th 2016

I mean the proof that $P: E^{op} \to E$ is monadic, which is the standard approach (see, e.g., Mac Lane-Moerdijk); I believe this result is usually credited to Paré.

• CommentRowNumber9.
• CommentAuthorTodd_Trimble
• CommentTimeMar 29th 2016

Okay, I’ve created a first installment at quotient object, indicating a Galois connection between quotient objects and binary relations.

I may be adding more later.

• CommentRowNumber10.
• CommentAuthorThomas Holder
• CommentTimeMar 29th 2016
• (edited Mar 29th 2016)

The reference for Paré is:

Robert Paré, Colimits in Topoi , Bull. AMS 80 (1974) pp.556-661. (pdf)

This has the by now standard proof but the result itself is attributed to Mikkelsen, a student of Anders Kock, in Johnstone’s 1977 book.

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeMar 30th 2016

Thomas, thanks a lot for the reference! That’s what I was looking for. I have added a pointer at quotient type.

Todd, thanks for your additions to quotient object. What I think would be particularly useful to eventually add to the nLab is discussion of how quotients may be constructed using a subobject classifier. If you would find time to get to that, that would be a big service, I think.

• CommentRowNumber12.
• CommentAuthorTodd_Trimble
• CommentTimeMar 30th 2016

Urs, as I said, this was a first installment. A full write-up will take some time. I’ve been thinking though that it should probably have its own article (i.e., it won’t all fit comfortably at quotient object or at elementary object), although maybe I can sketch just the construction at quotient object.

• CommentRowNumber13.
• CommentAuthorTodd_Trimble
• CommentTimeMar 30th 2016

Okay, you can now have another look at quotient object. I have added a subsection “In toposes”.

Obviously this is just in outline form for now.

• CommentRowNumber14.
• CommentAuthorUrs
• CommentTimeMar 30th 2016
• (edited Mar 30th 2016)

Thanks, Todd!!

• CommentRowNumber15.
• CommentAuthorRodMcGuire
• CommentTimeMar 31st 2016

Off topic but related. I came across generalized kernel while looking for information about quotients in enriched categories.

It contains the unknown iTeX ulcorner f urcorner which has been present since Mike Shulman started that page in 2012.

Is there some other notational convention, say a hat, that could be used there?

• CommentRowNumber16.
• CommentAuthorMike Shulman
• CommentTimeAug 2nd 2018

Reference Hofmann’s thesis for “higher inductive” quotients (predating general HITs), and mention Maietti’s result that “effectiveness” for quotients of “Type-valued equivalence relations” implies LEM.