Thomas Streicher. Investigations into Intensional Type Theory. Habilitation Thesis, Ludwig-Maximilians-Universität München, 1993. https://www2.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf