added pointer to:

- Bart Jacobs, Chapter 6 in:
*Categorical Logic and Type Theory*, Studies in Logic and the Foundations of Mathematics**141**, Elsevier (1998) [ISBN:978-0-444-50170-7, pdf]

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

]]>