Skip to main content
PRL Project

Set-theoretical models of type theory

by Wojciech Moczydlowski

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.

Aczel paper