# 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.