Triposes, q-toposes and toposes

https://doi.org/10.1016/j.apal.2014.10.005Get rights and content
Under an Elsevier user license
open archive

Abstract

We characterize the tripos-to-topos construction of Hyland, Johnstone and Pitts as a biadjunction in a 2-category enriched category of equipment-like structures. These abstract concepts are necessary to handle the presence of oplax constructs – the construction is only oplax functorial on a certain class of tripos morphisms.

A by-product of our analysis is the decomposition of the tripos-to-topos construction into two steps, the intermediate step being a generalization of quasitoposes.

MSC

03G30
03B15
18D05

Keywords

Tripos-to-topos construction
Quasitopos
Proarrow equipment

Cited by (0)

1

The author gratefully acknowledges support of the ERC Advanced Grant ECSYM.