Remarks on the tripos to topos construction: comprehension, extensionality, quotients and functional-completeness (Q263883)

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.