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

2014/01/30 by Fabio Pasquali, Pasquali, Fabio
Computer Science · Mathematics · #Advanced Algebra and Logic #Advanced Topology and Set Theory #Homotopy and Cohomology in Algebraic Topology #math.CT #math.LO

paper · pdf · doi:10.48550/arxiv.1401.7867

arxiv created 2014/02/24 · arxiv updated 2014/02/25

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 \citefrey and that of Carboni in \citecarbons are instances of this one.

Related

• A 2-Categorical Analysis of the Tripos-to-Topos Construction
• A Very Short Introduction to Topos Theory (adapted from Prof. Pettigrew's notes)
• Foundations of a Recent Extension of Category Theory and Topos Theory
• Representing the language of a topos as quotient of the category of spans
• Quasitoposes as elementary quotient completions