Re: Is equality evil?

[Michael Shulman <shulman@math.uchicago.edu>]

On Tue, Sep 21, 2010 at 9:00 PM, Toby Bartels
<toby+categories@ugcs.caltech.edu> wrote:
> In sufficiently impredicative mathematics, identity can be defined:
>  Given a type A and elements x and y of A, x is _identical_ to y
>  if, for every predicate p on A, p holds for x iff p holds for y.
> ...
> It would be interesting to hear from people who want to keep kosher,
> but also want to reason impredicatively, how to interpret this definition.

Well, if "for every predicate" is to be interpreted as ranging only
over kosher predicates, then x and y are Leibniz identical as soon as
they are isomorphic (or equivalent, or whatever is appropriate).  Note
that in order for the notion of "keeping kosher" to even be
meaningful, you need the type A to "come with" some sort of notion of
equivalence between its elements; assigning it after the fact isn't
good enough.  But if A does have such a notion, then it seems that
Leibniz identity is provably equivalent to "there exists an
equivalence between x and y," by applying the definition of Leibniz
identity to the property p(z) = "there exists an equivalence between x
and z".

> 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, this makes sense from the perspective above, since there's
no reason to expect that simply knowing that there *exists* an
equivalence between x and y would determine a map B(x) -> B(y); you
need to first pick a particular such equivalence.  I find this to be a
good reason for (intensional) identity types, whose elimination rule
provides a map (indeed, an equivalence) B(x) -> B(y) for any
inhabitant of Id(x,y).  In fact, the inductive notion of identity
types, as used in Voevodsky's foundations:

Inductive paths (T:Type)(t:T): T -> Type := idpath: paths T t t.

seems to me to essentially define it by strengthening Leibniz identity
to allow elimination into Set/Type as well.

Mike


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