Erik Palmgren: A setoid model of extensional Martin-Löf type theory in Agda
Tid: On 2019-01-30 kl 10.00 - 11.45
Föreläsare: Erik Palmgren, SU
Plats: Room 16, Building 5, Department of Mathematics, Kräftriket
Abstract: We present details of an Agda formalization of a setoid model of Martin-Löf type theory with Pi, Sigma, extensional identity types, natural numbers and a universe à la Russell. A crucial ingredient is the use of Aczel's type V of iterative sets as an extensional universe of setoids, which allows for a well-behaved interpretation of type equality.