Relating the Effective Topos to HoTT

The effective topos Eff was introduced by Martin Hyland in [4] and proved to be a very useful category where to test computational properties of constructive theories, see [9]. In the talk we present a way to see Eff as part of a model of Homotopy Type Theory [6]. The presentations of Eff as an exact completion and of its full subcategory Asm on the assemblies as a regular completion in [2] suggested that the topos might be obtained as a homotopy quotient of some appropriate category, see also [7]. This is understood in a very rough sense, based on the construction of the exact completion via the pseudo-equivalence relations of Aurelio Carboni as in [1]. By considering the category of the pseudo-equivalence relations in Asm (with graph homomorphisms), we can show that Eff is a full subcategory of the homotopy quotient Ho(Kan([C ,Asm])) of the category of Kan fibrant cubical assemblies, see [3, 5]. In fact, we obtain this from the stronger result that the extensional realizability topos Ext of [8], into which Eff embeds fully, is a full subcategory of Ho(Kan([C ,Asm])).