Abstract

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.