Fixed broken links to home page Ahrens

Anonymous

]]>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.

]]>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?

]]>Thanks, Todd!!

I have added some more hyperlinks and then I have cross-linked these two sections:

]]>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.

]]>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.

]]>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.

]]>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.

]]>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.

]]>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é.

]]>That would be great if you could add something.

What’s the precise citation to Paré?

]]>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é.

]]>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.

“Universal mapping property”, I believe.

]]>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.

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

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

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.

]]>