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.