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).
    • CommentRowNumber1.
    • CommentAuthorzskoda
    • CommentTimeJun 7th 2011
    • (edited Jun 7th 2011)

    In passing, I have added the Pitts’ thesis (pdf) to the literature on effective topos. I am not familiar with the concept, but came across in passing, so I do not understand the “The” effective topos qualification; the present entry makes impression of the uniqueness. If I did not misread those few sentences of the thesis which I actually read, one takes an arbitrary elementary topos EE with a natural numbers object and creates the “external” effective topos eEe E on EE. It says (page 82) that the correspondence EeEE\mapsto e E is part of a functor which has a canonically defined fully faithful right adjoint. Probably effective topos as it is now talks about the case of eEe E when E=SetE = Set.

    I have added the thesis also to the references at tripos and corrected the link to the other reference there. Added a person entry Andrew Pitts.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeJun 7th 2011

    Yes, “the” effective topos is generally used to refer to the one based on Set.

    • CommentRowNumber3.
    • CommentAuthorzskoda
    • CommentTimeJun 7th 2011
    • (edited Jun 7th 2011)

    Then the entry should be clear about that. The Pitts’ thesis which is according to some the second most important reference on the subject is looking it more generally. Edit: I added a quick repair, but not satisfactory, I am not clear how much of the first paragraph of effective topos makes sense in full generality.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJun 8th 2011

    It looks good to me now. I don’t know either how much of the first paragraph is valid in generality, and right now the page doesn’t appear to claim that any of it is.

    • CommentRowNumber5.
    • CommentAuthorzskoda
    • CommentTimeJun 8th 2011

    OK, hopefully some of us will once delve more into it :)

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2023

    added pointer to:

    diff, v19, current