Re: Is equality evil?

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

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.

It seems to me t that the point simply is that use of equality in premisses
can be avoided by declaring varibales appropriately. That trick goes a long
way in basic category theory.

Using Id-types is a different thing. Extensional Id-types together with sums
correspond to "cartesian logic" which suffices for declaring a lot of
categorical concepts.

Intensional Id-types might be convenient for providing a logic where equality
gets identified with isomorphism or even weak equivalence. But that's not
avoiding equality it's rather `liberal'ising it.

Thomas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]