Remarks on the Tripos To Topos Construction: extensionality, comprehensions, quotients and cauchy-complete objects
Fabio Pasquali

TL;DR
This paper analyzes the Tripos to Topos construction, showing it as a composition of four free constructions and relating it to similar existing constructions, thereby clarifying its structure and universality.
Contribution
It provides a new description of the Tripos to Topos construction as a composition of four free constructions and unifies it with similar known constructions.
Findings
The Tripos to Topos construction can be decomposed into four free constructions.
It forms a free functor from triposes to toposes.
The construction encompasses and generalizes previous similar constructions.
Abstract
We give a description of the Tripos To Topos construction in terms of four free constructions. We prove that these compose up to give a free construction from the category of triposes and logical morphisms to the category of toposes and logical functors. Then we show that other similar constructions, i.e. the one given by Frey in \cite{frey} and that of Carboni in \cite{carbons} are instances of this one.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsHomotopy and Cohomology in Algebraic Topology · Advanced Topology and Set Theory · Advanced Algebra and Logic
