I am investigating the category in which there happens to be no subobject classifier for the particular way in which it is formulated. But, there is an object however who is very close to a subobject classifier, and in fact, the subobjects that it is capable of classifying are sufficient to me for all intents and purposes. I call it for lack of better terminology : a partial subobject classifier.
I want to study some kind of language derived in the style of the Mitchell-Benabou language for a topos, but that can characterize only those subobjects given by my partial subobject classifier.
Does that make any sense?
So, my question is :
First of all, does that seem feasible to obtain a Mitchell-Benabou language on a ``partial subobject classifier’’; that is, an object whose elements only classify a specific class of subobjects?
Secondly, what are the complications I might have to deal with in the measure in which it is feasible?
Remark : I'm pretty sure this partial subobject classifier has an internal complete Heyting algebra structure, so that part isn't a problem. I still have some work to do on checking how dependent types will arise... but then, what else could there be?