"Construction and deduction in type theories."

Martin Strecker (1999)
a service of Schloss Dagstuhl - Leibniz Center for Informatics