Loïc Pujet: On Fragments of Choice and Setoid Models of Type Theory
Tid: On 2025-03-19 kl 10.00 - 12.00
Plats: Albano house 1, floor 3, Room U (Kovalevsky)
Medverkande: 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.