## References {: #ckvw98change } * Carboni, A., Kelly, G. M., Verity, D. and Wood, R. J. A 2-categorical approach to change of base and geometric morphisms II. _TAC_ 4(5), 1998. {: #jacobs99cltt } * Jacobs, B. _Categorical Logic and Type Theory_, Elsevier 1999. {: #elephant } * Johnstone, P. T. _Sketches of an Elephant: A Topos Theory Compendium_, OUP 2002. {: #gp99limits } * Grandis, M. and Paré, R. Limits in double categories. _Cahiers_ 40(3), 1999. {: gp04adjoint } * Grandis, M. and Paré, R. Adjoint \[sic\] for double categories. _Cahiers_ 45(3), 2004. {: kelly05enriched } * Kelly, G. M. _Basic Concepts of Enriched Category Theory_. _TAC_ Reprints, 2005. {: #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. ([PDF](http://www.math.mcgill.ca/~rags/ZML/ZML.PDF)). {: #shulman08framed } * [[nlab:Mike Shulman|Shulman, M]]. Framed bicategories and monoidal fibrations. _TAC_ 20(18), 2008. {: #wood82proarrowsi } * Wood, R.J. Abstract proarrows I. _Cahiers_ 23(3), 1982. ### Abbreviations _Cahiers_ : [Cahiers de topologie et géométrie différentielle catégoriques](http://www.numdam.org/numdam-bin/feuilleter?j=CTGDC) _TAC_ : [Theory and Applications of Categories](http://www.tac.mta.ca/tac/) _TAC_ Reprints : [Reprints in Theory and Applications of Categories](http://www.tac.mta.ca/tac/reprints/index.html)