A universal characterization of the tripos-to-topos construction
Jonas Frey (Paris 7)
The concept of (elementary) topos was introduced by Lawvere and Tierney around 1970 as a generalization of Grothendieck's notion of topos (nowadays known as Grothendieck topos), motivated by logical and foundational questions. Nevertheless, until 1980, all known toposes were in fact Grothendieck toposes, so the greater generality of Lawvere/Tierney's definition was never really exploited. Finally, in 1980, Hyland, Johnstone and Pitts described a construction which gives rise to toposes other than Grothendieck toposes. This construction starts from "triposes", which are certain fibrations used in categorical logic. The most prominent topos that can be obtained in this way is the "effective topos", which was described in an article by Hyland in 1981.
I will begin my talk by giving a detailed and elementary description of the effective topos, using a decomposition of Hyland's original construction in two steps. Then I will define the general concept of "tripos", and explain how the decomposition of the construction which was demonstrated at the example of the effective topos allows us to give a characterization of the tripos-to-topos construction as a kind of biadjunction between a 2-category of triposes and a 2-category of toposes.
