Erik Palmgren: What is an internal setoid model of dependent type theory?
Erik Palmgren, Stockholm University
Tid: On 2012-03-07 kl 10.00 - 11.45
Plats: SU, Kräftriket, building 5, room 16
Standard models of dependent type theory, such as categories with attributes, use semantics based on the category of sets. It seems to be an unresolved question how to best formulate such semantics using the category of setoids instead, and how to do this internally to type theory it self.
We discuss some proposals for solutions and possible generalizations to other categories of interpretation.