Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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 $E$ with a natural numbers object and creates the “external” effective topos $e E$ on $E$. It says (page 82) that the correspondence $E\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 $e E$ when $E = 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.
Yes, “the” effective topos is generally used to refer to the one based on Set.
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.
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.
OK, hopefully some of us will once delve more into it :)
added pointer to:
1 to 6 of 6