Re: Is equality evil?

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

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/ ]