A Category Theoretic Analysis of Predicative Type Theory. - Michael Schwartzbach (1987)