I suspected already that you want to use no identity types at all. Well, in category theory one needs at least equality on morphisms. What I meant was that when one just considers finite types over a base type (typically N) one can use an equality defined by recursion on the type structure. But that's an ontology good for analysis and not for category theory. Moreover, there will be maps between these types which don't respect the inductively defined equality. Alternatively, one coud work with setoids as suggested by Palmgren. But that has also its intricacies since the binary predicates forming part of setoids are proof-relevant in general (see Palmgren's posting). As to Leibniz equality. If x and y are Leibniz equal, i.e. \forall P : A -> Prop. P(x) -> P(y), then this doesn't allow one to construct a map B(x) -> B(y) in case B : A -> Set (simply because Set is not Prop). Of course, dropping impredicativity you loose the theory of toposes. But maybe that's not so bad since van den Berg and Moerdijk have developed predicative algebraic set theroy in a sequence of papers available on the arXiv. Predicative topos theory is less well developed. But notice that they work with extensional equality (expressed by the reqirement that regular monos are small). I must say I remain unconvinced about working without equality as long as I haven't seen a convincing account of (presheaf) toposes and fibered categories in such a restricted setting. But presumably, people have other application areas in mind. It would be interesting to identify those. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]