6
$\begingroup$

I have one other reference request (cf. my previous question: Topos theory reference suitable for undergraduates)

Are there any references on effective topoi that are better than Hyland's original paper:

The effective topos J.M.E. Hyland, in: Troelstra and Van Dalen (eds), The L.E.J.Brouwer Centenary Symposium, North-Holland 1982, 216.

Improve this question
$\endgroup$

3 Answers 3

Reset to default
8
$\begingroup$

Realizability: An Introduction To Its Categorical Side by Jaap van Oosten is all about realizability toposes.

There are some lecture notes online by Wesley Phoa entitled An introduction to fibrations, topos theory, the effective topos and modest sets, which do exactly what it says on the tin.

There is also some good material in Freyd and Scedrov's book Categories, Allegories.

Improve this answer
$\endgroup$
4
  • 2
    $\begingroup$ Wesley Phoa's lecture notes are at lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208 $\endgroup$
    – Andrej Bauer
    Commented Feb 18, 2011 at 22:12
  • $\begingroup$ Colling McLarty's book "Elementary categories, elementary toposes" treats the effective topos, too. $\endgroup$
    – Andrej Bauer
    Commented Feb 18, 2011 at 22:13
  • $\begingroup$ I found both the Phoa notes and the Jaap van Oosten book extremely helpful. The McLarty and the Freyd/Scedrov I like in general, but I didn’t find them especially useful in this particular connexion. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Feb 19, 2011 at 4:14
  • 1
    $\begingroup$ I think Freyd--Scedrov may be a good starting point for understanding the exact-completion construction of the effective topos, which is less often discussed than the tripos-to-topos version. Other good resources for this are the paper A categorical approach to realizability and polymorphic types by Carboni, Freyd and Scedrov, Carboni's Some free constructions in realizability and proof theory, and Robinson and Rosolini's Colimit completions and the effective topos. $\endgroup$
    – Finn Lawler
    Commented Feb 19, 2011 at 17:15
5
$\begingroup$

I'd prefer not to discuss "better" but another useful treatment of the effective topos is in the book "Categorical Logic and Type Theory" by Bart Jacobs (particularly Chapter 6).

Improve this answer
$\endgroup$
4
$\begingroup$

Andrew Pitts’ note “Tripos Theory in Retrospect” sheds some useful light on $\mathcal{Eff}$, from a slightly different angle than most other books do. It’s available at his publications page, and also at doi:10.1017/S096012950200364X (paywalled but potentially more durable).

For my part, even as quite a toposophile, $\mathcal{Eff}$ (and realizability toposes in general) took me a while to get comfortable with — a lot longer than any of the other genres, sheaves, syntactic ones, etc. In the end it must have taken about four or five attempts to get to grips with them, over several years — spending a little time getting a little way on each attempt, understanding one step in the construction (e.g.: the tripos-to-topos step in general), then waiting a few months while that sank in, before coming back for another crack at the next step. This certainly isn’t everyone’s experience, of course, but I’ve talked to at least a couple of other people who had a similar time.

Improve this answer
$\endgroup$
1
  • 3
    $\begingroup$ This is encouraging. It suggests that I'll eventually understand the effective topos if I keep trying. $\endgroup$
    – Andreas Blass
    Commented Feb 19, 2011 at 16:20

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .