Triposes, q-toposes and toposes

摘要

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.