intensional higher-order logic

intensional higher-order logic

[Tom Hirschowitz]

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.