Thanks Thomas for bringing up the intensional type theory perspective. Here equality of objects in categories is a serious problem already for sets, or rather for their type theoretic counterpart, setoids (types with equivalence classes). The so-called identity types give a minimal equality on each type A: Id(A,a,b) are the proofs that a and b are equal in A. But the fact that these proofs are in general not unique and induces a groupoid structure makes it difficult to apply when e.g. A is a universe of types. Some remarks are contained in in this preprint http://www.mittag-leffler.se/preprints/files/IML-0910f-36.pdf If one tries to use the Id-types to define equality on (small) setoids one ends up with a groupoid of objects rather than a setoid objects. I think the situation can be described as follows for a general category K, which we think of as a category without equality of objects. We now want to induce an equality of objects on (a part of) K. Take a groupoid G and a functor F:G -> K. We define the groupoids of objects C_0, arrows C_1 and composable arrows C_2 in a natural way. C_0 is G and C_1 has for objects triples (a,b,f) where a,b in G and f:F(a) -> F(b), and a morphism (a,b,f) -> (a',b',f') is a pair of G morphisms r:a -> a' and s:b -> b' with F(s) f = f' F(r). C_2 has for objects pairs of morphisms composable with an mediating map m from G, i.e. ((a,b,f),(c,d,g),m). The composition is g F(m)f. The morphisms of C_2 are then pairs of C_1 morphisms ((r,s), (t,u)): ((a,b,f),(c,d,g),m) -> ((a',b',f'),(c',d',g'),m') with m's= t m. When G is a discrete groupoid this becomes a standard category. When G is a groupoid it becomes almost a category. Notions of limits can be formulated in a natural fashion. At least when K=Setoids, C inherits limits from K. Perhaps some general results are known about this construction of C from functor F:G -> K on a groupoid G? Erik
It's no problem to come up with logics without equality predicates. Just omit the equality predicate and its associated axioms. For ideological reasons most logic texts give equality a distinguished status for historical reasons. In case of extensional theories it suffices to have equality on base type and lift it `a la logical relations. But then there might be operations which don't respect this kind of equality. In other words identity types are not necessary for doing constructive mathematics. Intensional Id-types arise from putting the idea to an extreme that all logical concepts are "inductively defined", i.e. are given by constructors and eliminators. The notion of equality of types you refer to is a different one. Namely judgemental equality which cannot be used as an ingredient for forming propositions.
...... [For admin and other information see: http://www.mta.ca/~cat-dist/ ]