A characterization of generalized existential completions

Banaschewski, 1991, Projective and supercoherent frames, J. Pure Appl. Algebra, 70, 45, 10.1016/0022-4049(91)90005-M

Biering, 2008

Carboni, 1995, Some free constructions in realizability and proof theory, J. Pure Appl. Algebra, 103, 117, 10.1016/0022-4049(94)00103-P

Carboni, 1998, Regular and exact completions, J. Pure Appl. Algebra, 125, 79, 10.1016/S0022-4049(96)00115-6

Cockett, 2002, Restriction categories I: categories of partial maps, Theor. Comput. Sci., 270, 223, 10.1016/S0304-3975(00)00382-0

Emmenegger, 2020, Elementary doctrines as coalgebras, J. Pure Appl. Algebra, 224, 10.1016/j.jpaa.2020.106445

Frey, 2022, Categories of partial equivalence relations as localizations, J. Pure Appl. Algebra

Gödel, 1986

Hofstra, 2006, All realizability is relative, Math. Proc. Camb. Philos. Soc., 141, 239, 10.1017/S0305004106009352

Hofstra, 2011, The dialectica monad and its cousins, vol. 53, 107

Hughes, 2003, Factorization systems and fibrations: toward a fibered Birkhoff variety theorem, Electron. Notes Theor. Comput. Sci., 69, 156, 10.1016/S1571-0661(04)80564-4

Hyland, 1982, The effective topos, vol. 110, 165

Hyland, 1980, Tripos theory, Math. Proc. Camb. Philos. Soc., 88, 205, 10.1017/S0305004100057534

Jacobs, 1999, Categorical Logic and Type Theory, vol. 141

Johnstone, 1982, Stone Spaces

Johnstone, 2002, Sketches of an Elephant: A Topos Theory Compendium, vol. 2

Kelly, 1992, A note on relations relative to a factorisation system, 249

Lawvere, 1969, Adjointness in foundations, Dialectica, 23, 281, 10.1111/j.1746-8361.1969.tb01194.x

Lawvere, 1970, Equality in hyperdoctrines and comprehension schema as an adjoint functor, 1

Maietti, 2017, Triposes, exact completions, and Hilbert's ϵ-operator, Tbil. Math. J., 10, 141

Maietti

Maietti, 2013, Elementary quotient completion, Theory Appl. Categ., 27, 445

Maietti, 2013, Quotient completion for the foundation of constructive mathematics, Log. Univers., 7, 371, 10.1007/s11787-013-0080-2

Maietti, 2015, Unifying exact completions, Appl. Categ. Struct., 23, 43, 10.1007/s10485-013-9360-5

Maietti, 2016, Relating quotient completions via categorical logic, 229

Maietti

Mulry, 1992, Partial map classifiers and partial cartesian closed categories, Theor. Comput. Sci., 99, 141, 10.1016/0304-3975(92)90176-G

Pitts, 1995, Categorical logic, vol. 6, 39

Pitts, 2002, Tripos theory in retrospect, Math. Struct. Comput. Sci., 12, 265, 10.1017/S096012950200364X

Robinson, 1988, Categories of partial maps, Inf. Comput., 79, 94, 10.1016/0890-5401(88)90034-X

Rosolini, 1985, Domains and dominical categories, Riv. Mat. Univ. Parma, 11, 387

Rosolini, 1986

Streicher, 2018, Realizability

Trotta, 2020, The existential completion, Theory Appl. Categ., 35, 1576

Trotta

Trotta, 2021, The Gödel fibration, vol. 202, 87:1

Trotta, 2022, Dialectica logical principles, 346

Trotta, 2022, Dialectica logical principles: not only rules, J. Log. Comput., 10.1093/logcom/exac079

van Dalen, 2004, Logic and Structure, 10.1007/978-3-540-85108-0

van Oosten, 1997, The modified realizability topos, J. Pure Appl. Algebra, 116, 273, 10.1016/S0022-4049(97)00101-1

van Oosten, 2008, Realizability: An Introduction to Its Categorical Side, vol. 152