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. 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. (C) 2014 Elsevier B.V. All rights reserved.