New preprint : A model of Martin-Löf extensional type theory with universes formalized in Agda ( arXiv:1909.01414)

[Erik Palmgren]

From type theory to setoids and back

Erik Palmgren

(Submitted on 3 Sep 2019)

A model of Martin-Löf extensional type theory with universes is formalized in Agda, an interactive proof system based on Martin-Löf intensional type theory. This may be understood, we claim, as a solution to the old problem of modelling the full extensional theory in the intensional theory. Types are interpreted as setoids, and the model is therefore a setoid model. We solve the problem of intepreting type universes by utilizing Aczel's type of iterative sets, and show how it can be made into a setoid of small setoids containing the necessary setoid constructions. 
In addition we interpret the bracket types of Awodey and Bauer. Further quotient types should be interpretable.

Comments:	30 pages
Subjects:	Logic (math.LO)
MSC classes:	03B15, 03B35, 03E70, 03F50
Cite as:	arXiv:1909.01414 [math.LO]
	(or arXiv:1909.01414v1 [math.LO] for this version)

https://arxiv.org/abs/1909.01414