Jacopo Emmenegger Explores Effective 2-Topos and Hyland's Model 📚

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.

Recording during the thematic meeting : «Synthetic mathematics, logic-affine computation and efficient proof systems» the September 09, 2025 at the Centre International de Rencontres Mathématiques (Marseille, France)

Filmmaker : Luca Récanzone

Find this video and other talks given by worldwide mathematicians on CIRM's Audiovisual Mathematics Library: http://library.cirm-math.fr. And discover all its functionalities: - Chapter markers and keywords to watch the parts of your choice in the video - Videos enriched with abstracts, bibliographies, Mathematics Subject Classification - Multi-criteria search by author, title, tags, mathematical area