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

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.