Unifying Exact Completions

Barr, M.: Exact categories. In: Barr, M., Grillet, P., van Osdol, D. (eds.) Exact Categories and Categories of Sheaves. Lecture Notes in Mathematical, vol. 236, pp. 1–120. Springer-Verlag (1971)

Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13(2), 261–293 (2003)

Carboni, A.: Analysis non-standard e topos. Rend. Istit. Mat. Univ. Trieste 14(1–2), 1–16 (1982)

Carboni, A.: Some free constructions in realizability and proof theory. J. Pure Appl. Algebra 103, 117–148 (1995)

Carboni, A., Celia Magno, R.: The free exact category on a left exact one. J. Aust. Math. Soc. 33(A), 295–301 (1982)

Carboni, A., Freyd, P., Scedrov, A.: A categorical approach to realizability and polymorphic types. In: Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) Mathematical Foundations of Programming Language Semantics. Lectures Notes in Computer Science, vol. 298, pp. 23–42. Springer-Verlag, New Orleans (1988)

Carboni, A., Vitale, E.: Regular and exact completions. J. Pure Appl. Algebra 125, 79–117 (1998)

Carboni, A., Walters, R.: Cartesian bicategories. J. Pure Appl. Algebra 49, 11–32 (1987)

Coquand, T.: Metamathematical investigation of a calculus of constructions. In: Odifreddi, P. (ed.) Logic in Computer Science, pp. 91–122. Academic Press (1990)

Frey, J.: A 2-categorical analysis of the tripos-to-topos construction. arXiv: 1104.2776v1 [math.CT] (2011)

Freyd, P., Scedrov, A.: Categories Allegories. North Holland Publishing Company (1991)

Hughes, J., Jacobs, B.: Factorization systems and fibrations: toward a fibred Birkhoff variety theorem. Electron. Notes Theor. Comput. Sci. 11 (2002)

Hyland, J.M.E., Johnstone, P.T., Pitts, A.M.: Tripos theory. Math. Proc. Camb. Phil. Soc. 88, 205–232 (1980)

Jacobs, B.: Categorical Logic and Type Theory. North Holland Publishing Company (1999)

Kelly, G.: A note on relations relative to a factorization system. In: Carboni, A., Pedicchio, M., Rosolini, G. (eds.) Category Theory ’90. Lecture Notes in Mathematical, vol. 1488, pp. 249–261. Springer-Verlag, Como (1992)

Lawvere, F.W.: Adjointness in foundations. Dialectica 23, 281–296 (1969)

Lawvere, F.W.: Diagonal arguments and cartesian closed categories. In: Category Theory, Homology Theory and their Applications, II (Battelle Institute Conference, Seattle, Wash., 1968, Vol. Two), pp. 134–145. Springer (1969)

Lawvere, F.W.: Equality in hyperdoctrines and comprehension schema as an adjoint functor. In: Heller, A. (ed.) Proceedings New York Symposium on Application of Categorical Algebra, pp. 1–14. American Mathematical Society (1970)

Lawvere, F.W., Rosebrugh, R.: Sets for Mathematics. Cambridge University Press (2003)

Maietti, M.: A minimalist two-level foundation for constructive mathematics. Ann. Pure Appl. Logic 160(3), 319–354 (2009)

Maietti,M., Rosolini, G.: Elementary quotient completion. Theory Appl. Categ. 27(17), 445–463 (2013)

Maietti, M., Rosolini, G.: Quotient completion for the foundation of constructive mathematics. Log. Univers. 7(3), 371–402 (2013)

Maietti, M.E.: Joyal’s arithmetic universe as list-arithmetic pretopos. Theory Appl. Categ. 3(24), 39–83 (2010)

Nordström, B., Petersson, K., Smith, J.: Programming in Martin Löf’s Type Theory. Clarendon Press, Oxford (1990)

Pasquali, F.: A co-free construction for elementary doctrines. To appear in Applied Categorical Structures (2013)

Pitts, A.M.: Tripos theory in retrospect. Math. Struct. Comput. Sci. 12(3), 265–279 (2002)

Succi Cruciani, R.: La teoria delle relazioni nello studio di categorie regolari e di categorie esatte. Riv. Mat. Univ. Parma (4) 1, 143–158 (1975)

van Oosten, J.: Realizability: An Introduction to its Categorical Side, vol. 152. North Holland Publishing Company (2008)