Remarks on the tripos to topos construction: comprehension, extensionality, quotients and functional-completeness. (English) Zbl 1345.18001

Pasquali, Fabio

Appl. Categ. Struct. 24, No. 2, 105-119 (2016).

The classical tripos to topos construction, which canonically extends a tripos to obtain a topos completing it, is studied in this article. The result is a chain of four free constructions that, when composed together, provide the classical construction.
The significance of the decomposition is that it neatly separates the degrees of information which are needed to perform the classical construction, making clear how the completion process develops in stages, each one being a simple step, in a technical sense, i.e., a free functor.
Each functor enriches the structure with a specific property: the first functor adds full comprehension to the tripos; the second functor in the chain extends a tripos having full comprehension with extensional equality; the third functor adds effective quotients; finally, the last functor in the chain enriches the structure obtained so far from the tripos with a functional complete basis. The composition of these four functors, which from the category of triposes and logical functors to the category of elementary toposes and logical functors, provides the classical construction. The forgetful functors, which are the counterparts of the four functors above in the free adjunction, are the natural ones, forgetting the previously mentioned properties from the topos structure.
In the conclusion, the paper discusses the relation of the present work to Carboni’s results, and concludes considering what happens when geometric functors are considered instead of logical functors.

Reviewer: Marco Benini (Buccinasco)

MSC:

18B25	Topoi
03G30	Categorical logic, topoi

Keywords:

tripos theory; categorical logic

References:

[1]	Carboni, A; Vitale, EM, Regular and exact completions, J. Pure Appl. Algebra, 125, 79-116, (1998) · Zbl 0891.18002
[2]	Carboni, A, Nonstandard analysis and topoi, Rend. Istit. Mat. Univ. Trieste, 14, 1-16, (1982)
[3]	Frey, J.: A 2-categorical analysis of the tripos-to-topos construction. arXiv:1104.2776 (2011) · Zbl 0451.03027
[4]	Grothendieck, A.: Revêtements étales et groupe fondamental (SGA 1), volume 224 of Lecture notes in mathematics. Springer-Verlag (1971)
[5]	Higgs, D.: A category approach to boolean-valued set theory (1973) · Zbl 0891.18002
[6]	Hyland, J.M.E.: The effective topos In: The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), volume 110 of Stud. Logic Foundations Math., pp. 165-216. North-Holland, Amsterdam-New York (1982)
[7]	Hyland, JME; Johnstone, PT; Pitts. A.M., Tripos theory., Math. Proc. Camb. Phil. Soc., 88, 205-232, (1980) · Zbl 0451.03027
[8]	Jacobs, B.: Categorical Logic and Type Theory, volume 141 of Studies in Logic and the foundations of mathematics. North-Holland Publishing Co. (1999)
[9]	Scott, D.S., Fourman, M.P.: Sheaves and logic In: Applications of Sheaves, volume 753 of Application of sheaves, pp. 302-401 (1979) · Zbl 0415.03053
[10]	Maietti, ME; Rosolini, G, Elementary quotient completion, Theory Appl. Categ., 27, 445-463, (2013) · Zbl 1288.03048
[11]	Maietti, ME; Rosolini, G, Quotient completion for the foundation of costructive mathematics, Log. Univers., 7, 371-402, (2013) · Zbl 1288.03049
[12]	Pitts, A.M.: The Theory of Triposes. University of Cambridge, PhD thesis (1981)
[13]	Pitts, AM, Tripos theory in retrospect, Math. Struct. in Comp. Sci., 12, 265-279, (2002) · Zbl 1005.18005
[14]	Taylor, P.: Practical foundations of mathematics, volume 59 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge (1999)
[15]	van Oosten, J.: Realizability: An Introduction to its Categorical Side, volume 152 of Studies in Logic and the foundations of mathematics. North-Holland Publishing Co. (2008) · Zbl 0891.18002