Toby Bartels wrote:

Right. I would prefer to use no identity types at all. If there is a particular predicate (on some particular type) that you would like to think of as equality (on that type), then write down its definition and introduce a symbol for it.

If any (well-behaved) equivalence relation can be thought of as equality then it would seem to follow that equality is relative. That is: 1) A and B may be the same thing from one point of view and two different things from another point of view, 2) the cardinality of {A, B} may be either 1 or 2 depending on what point of view one takes, and 3) it may be that from one point of view there is no property that distinguishes A from B while from another point of view there is a property P that distinguishes A from B (for consistency I guess one has to say that relative to the first viewpoint, not only does P not exist, but the second viewpoint also fails to exist). In the philosophical literature the idea that equality/identity is relative is credited to philosopher Peter Geach (I can give a list of references if anyone is interested). It has few adherents, but maybe category theory can make it popular. Best regards, Mattias [For admin and other information see: http://www.mta.ca/~cat-dist/ ]