Hyland's effective topos Eff models extensional type theory with an impredicative universe of propositions, as it does any (elementary) topos. Remarkably, it contains another impredicative universe which turns out not to be a poset, that of so-called modest sets. This fact ensures that Eff also models type theories like System F and the Calculus of Constructions. Impredicative encodings of type constructors, while very economical, often fail to satisfy a certain uniqueness principle (the so-called eta-rules) and, in turn, do not have dependent eliminators and thus do not support proofs by induction. Awodey, Frey and Speight have shown how to use a univalent impredicative universe to produce encodings that do enjoy (propositional) eta-rules and dependent eliminators. It is then
natural to look for a semantic setting where to carry out such encodings. Current approaches to higher versions of Eff often take simplicial or cubical sets inside Eff or inside its subcategory of
assemblies. It was shown, however, that the subcategory of 0-types (the sets) in these higher toposes is not Eff. I will present work in progress with Steve Awodey where we construct a candidate effective 2-topos that does contain Eff as its subcategory of 0-types. An infinity version of this construction is being investigated by Anel, Awodey and Barton.
