Triposes, q-toposes and toposes

TY - JOUR

T1 - Triposes, q-toposes and toposes

AU - Frey, Jonas

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

U2 - 10.1016/j.apal.2014.10.005

DO - 10.1016/j.apal.2014.10.005

M3 - Journal article

SN - 0168-0072

VL - 166

SP - 232

EP - 259

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

IS - 2

ER -