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

Fabio Pasquali

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 tripo…