{: #jacobs99cltt } * Jacobs, B. _Categorical Logic and Type Theory_, Elsevier 1999. {: #elephant } * Johnstone, P. T. _Sketches of an Elephant: A Topos Theory Compendium_, OUP 2002. {: #pavlovic96maps } * Pavlovic, D. Maps II: Chasing diagrams in categorical proof theory. _Logic Journal of the IGPL_, 4(2), 1996. {: #prawitz65natded } * Prawitz, D. _Natural Deduction: A Proof-Theoretical Study_. Almqvist & Wiksell, 1965. {: #seely83hyper } * Seely, R. A. G. Hyperdoctrines, natural deduction and the Beck condition. _Zeitschr. f. math. Logik und Grundlagen der Math._, 29:505--542, 1983.