Loïc Pujet: On Fragments of Choice and Setoid Models of Type Theory
Time: Wed 2025-03-19 10.00 - 12.00
Location: Albano house 1, floor 3, Room U (Kovalevsky)
Participating: Loïc Pujet
Abstract
It is a well known fact that the axiom of choice is provable intensional type theory. However, it would be more accurate to say that the *intensional* axiom of choice is provable, while the *extensional* axiom remains out of reach. In this talk, I will discuss some fragments of choice and the extent to which they are compatible with extensionality, impredicativity, and the computation rules of intensional type theory.