Dear all, Here is a probably easy question on categorical logic. If I understood correctly from Bart Jacobs' book [1], a topos, besides its elementary definitions, e.g., as a complete CCC with a subobject classifier, may be defined as a category whose subobject fibration is a higher-order fibration. Such subobject higher-order fibrations always have extensional entailment, in the sense that logical equivalence implies internal equality (which in HOL is necessarily Leibniz equality modulo iso). My question is twofold: (a) Is there an intensional equivalent to the notion of topos? In other words, is there a widely accepted categorical, elementary characterization of HOL? (b) If so, for these HOL categories, is there an analogue of the definition in terms of subobject fibrations? For instance, is it the case that for such HOL categories, e.g., the fibration of monos (or the codomain fibration) is a higher-order fibration? The question might be equivalent to: is there a well-established pair of a fibred construction F and an elementary doctrine D, such that for all category C, C is in D iff F (C) is a HO fibration? However, I am highly unsure that this formulation makes sense. Thanks and all that, Tom [1] B. Jacobs, Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, North Holland, Elsevier, 1999.