Set-theoretical models of type theory
by Wojciech Moczydlowski
2004-2005
I will present the ideas from Peter Aczel's paper "On relating type theories and set theories" on constructing set-theoretical models for various type theories, which could be seen as approximations for type theories used in real-life provers, such as Coq and Nuprl.