From Type Theory to Setoids and Back
- Date: Wednesday 31 October 2018, 16:15 – 17:15
- Location: Roger Stevens LT 08 (9.08)
- Type: Logic, Seminars, Pure Mathematics
- Cost: Free
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.