Remarks on the Tripos To Topos Construction: extensionality, comprehensions, quotients and cauchy-complete objects
Category Theory
2014-02-25 v2 Logic
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.
Keywords
Cite
@article{arxiv.1401.7867,
title = {Remarks on the Tripos To Topos Construction: extensionality, comprehensions, quotients and cauchy-complete objects},
author = {Fabio Pasquali},
journal= {arXiv preprint arXiv:1401.7867},
year = {2014}
}