added pointer to:
OK, hopefully some of us will once delve more into it :)
]]>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.
]]>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.
]]>Yes, “the” effective topos is generally used to refer to the one based on Set.
]]>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 with a natural numbers object and creates the “external” effective topos on . It says (page 82) that the correspondence 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 when .
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.
]]>