Aczel's Type-Theoretic Interpretation of Constructive Zermelo-Fraenkel Set Theory
Dominik Wehr

Abstract:
In this report, we summarize Peter Aczel’s papers on the interpretation of constructive ZF into Martin Löf type theory. We aim to modernize some of the presentation and unify the various constructions into a coherent whole.