Timeline for The effective topos - by Hyland
Current License: CC BY-SA 2.5
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 19, 2011 at 17:15 | comment | added | Finn Lawler | 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. | |
| Feb 19, 2011 at 4:14 | comment | added | Peter LeFanu Lumsdaine | 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. | |
| Feb 18, 2011 at 22:13 | comment | added | Andrej Bauer | Colling McLarty's book "Elementary categories, elementary toposes" treats the effective topos, too. | |
| Feb 18, 2011 at 22:12 | comment | added | Andrej Bauer | Wesley Phoa's lecture notes are at lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208 | |
| Feb 18, 2011 at 20:57 | history | answered | Finn Lawler | CC BY-SA 2.5 |