Erik Palmgren: A setoid model of extensional Martin-Löf type theory in Agda
Time: Wed 2019-01-30 10.00 - 11.45
Location: Room 16, Building 5, Department of Mathematics, Kräftriket
Participating: Erik Palmgren, SU
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.