Skip to main content
expanded with my own story on learning Eff
Source Link

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.

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

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.

Source Link

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