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

2 views
Skip to first unread message

Erik Palmgren

unread,
Sep 5, 2019, 3:11:01 AM9/5/19
to homotopyt...@googlegroups.com


From type theory to setoids and back

(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)



Reply all
Reply to author
Forward
0 new messages