From Type Theory to Setoids and Back

Erik Palmgren, Stockholm University. Part of the logic seminar series.

Errett Bishop proposed several type-theoretic languages to be used for formalizing constructive mathematics.  The notion of set employed in Bishop-Bridges' book Constructive Analysis from 1985 is essentially a type with an explicitly defined equality.  This concept of set is also widely used in computer formalizations of mathematics under the name setoid.

Formalizing models of Martin-Löf type theory in itself provides a challenge for the development of the theory of setoids, as well as its implementation in proof assistants.  In this talk we report on progress on a setoid model.  Aczel's type-theoretic model of CZF plays an important role as an extensional universe of setoids.  We present some examples of our formalizations in the Agda proof-assistant.