Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore advanced concepts in topos theory and type theory through this 30-minute mathematical conference talk examining the construction of an effective 2-topos. Delve into Hyland's effective topos Eff and its remarkable properties, including how it models extensional type theory with impredicative universes and contains modest sets that enable modeling of System F and the Calculus of Constructions. Understand the limitations of impredicative encodings regarding eta-rules and dependent eliminators, and discover how Awodey, Frey and Speight's work with univalent impredicative universes addresses these challenges. Learn about current approaches to higher versions of Eff using simplicial or cubical sets and their limitations, particularly how the subcategory of 0-types in these higher toposes fails to be Eff. Follow the presenter's work-in-progress collaboration with Steve Awodey in constructing a candidate effective 2-topos that successfully contains Eff as its subcategory of 0-types, with insights into the ongoing infinity version investigation by Anel, Awodey and Barton. Gain exposure to cutting-edge research in synthetic mathematics and logic-affine computation presented at the Centre International de Rencontres Mathématiques thematic meeting on synthetic mathematics and efficient proof systems.
