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