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.