Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorzskoda
   • CommentTimeJun 7th 2011
   • (edited Jun 7th 2011)
   • PermaLink
   Author: zskoda
   Format: MarkdownItexIn passing, I have added the Pitts' thesis ([pdf](http://www.cl.cam.ac.uk/~amp12/papers/thet/thet.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]].

   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.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeJun 7th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexYes, "the" effective topos is generally used to refer to the one based on Set.

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

3. • CommentRowNumber3.
   • CommentAuthorzskoda
   • CommentTimeJun 7th 2011
   • (edited Jun 7th 2011)
   • PermaLink
   Author: zskoda
   Format: MarkdownItexThen 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.

   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.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeJun 8th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexIt 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.

   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.

5. • CommentRowNumber5.
   • CommentAuthorzskoda
   • CommentTimeJun 8th 2011
   • PermaLink
   Author: zskoda
   Format: MarkdownItexOK, hopefully some of us will once delve more into it :)

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

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeJan 22nd 2023
   • PermaLink
   Author: Urs
   Format: MarkdownItexadded pointer to: * [[Bart Jacobs]], Chapter 6 in: *Categorical Logic and Type Theory*, Studies in Logic and the Foundations of Mathematics **141**, Elsevier (1998) &lbrack;[ISBN:978-0-444-50170-7](https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/141), [pdf](https://people.mpi-sws.org/~dreyer/courses/catlogic/jacobs.pdf)&rbrack; <a href="https://ncatlab.org/nlab/revision/diff/effective+topos/19">diff</a>, <a href="https://ncatlab.org/nlab/revision/effective+topos/19">v19</a>, <a href="https://ncatlab.org/nlab/show/effective+topos">current</a>

   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]

   diff, v19, current