Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: quotient type

Bottom of Page

1 to 20 of 20

  1.  
    • 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→EP: 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!!

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

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

    diff, v10, current

  17. Fixed broken links to home page Ahrens

    Anonymous

    diff, v11, current

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeFeb 7th 2023

    added pointer to:

    diff, v12, current

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeFeb 7th 2023

    added pointer to:

    diff, v12, current

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeFeb 9th 2023
    • (edited Feb 9th 2023)

    I have moved the pointer to Li’s thesis to the top of the list of references, adding the lead-in

    On the convoluted history of the notion of quotient types, from setoids/Bishop sets to higher inductive types and in univalent foundations of mathematics:

    and added pointer also to Murray (2022, §4.3.2).

    I am not convinced of the subdivision of the following list of references into “As a higher inductive type” followed by “From univalence” which is inherited from previous versions, but I am leaving it as is for the time being.

    diff, v13, current

1 to 20 of 20

  1.