Re: Is equality evil?‏

Re: Is equality evil?‏

[Mattias Wikström]

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

Re: Is equality evil?

[Fred E.J. Linton]

Toby Bartels <toby+categories@ugcs.caltech.edu> wrote in part:
  
> The point is that one can recognise that two syntactic expressions,
> such as x and x, are the same, ...

Sorry, Toby, when I see "such as x and x" I have to struggle to
treat the expression between "as" and "and" as anything other than
different from the expression following the "and" -- for, if they
were really the same, there would be but one expression, not two,
it would be in one of those positions only, not both (I'm put in mind 
of the good old "Cheech and Chong"-ism, "How can you be in two places 
at once, if you're not anywhere at all?"), and you'd have used not 
the plural verb form "are" but the singular "is".

An illustration from another realm: each time the clerk behind the deli 
counter finishes with one customer and shouts "Next!" so as to bring up 
another one, the expression the clerk shouts refers to an entirely 
different customer than it did the time just before.

> ... or even that one reduces to another,
> such as fst(x,y) and x (where fst: A x B -> A is the usual projection),

Again I'm puzzled: what can fst(x,y) (where fst: A x B -> A is as you say)
possibly have to do with x (as in A x B, presumably -- or did you mean
as in fst(x,y), which could be problematic for void B)?

Sorry to be so obtuse, but ...; cheers, -- Fred



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

are fibrations evil?

[Thomas Streicher]

On the occasion of the discussion about "evil" I want to point out an example
where speaking about equality of objects seems to be indispensible.
If P : XX -> BB is a functor and one wants to say that it is a fibration
then one is inclined to formulate this as follows

     if u : J -> I is a map in BB and PX = I then there exists a morphism
     \phi : Y -> X with P\phi = u and \phi cartesian, i.e. ...

I don't see how to avoid reference to equality of objects in this formulation.

This already happens if XX and BB are groupoids where P : XX -> BB is a
fibration iff for all u : J -> I in BB and PX = I there is a map \phi : Y -> X
with P\phi = u.

Ironically the category of groupoids and fibrations of groupoids as families
of types was the first example of a model of type theory where equality may
be interpreted as being isomorphic.

So my conclusion is that equality of objects is sometimes absolutely
necessary. Avoiding reference to equality is also not a question of using
dependent types as some people implicitly seem to say. Even in intensional
type theory there is a notion of equality. But it is sometimes inconvenient
to use. As pointed out by Ahrens one can and should use extensional type theory
whenever convenient.
Intensional type theory allows one to interpret equality as being isomorphic,
a kind of reward for the inconvenience of using intensional identity types.

Thomas


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

Is equality evil?

[Vaughan Pratt]

Theorem.  Equality if and only if the diagonal.

Corollary.  P(equality) <--> P(contraction)

(where the predicate P may be "Evil", "Nonlinear", "Sophomoric", etc)

In this context (as opposed to metric spaces, materials, and maternity
wards) contraction is the logical rule predicated on the idea that two
things with the same name are actually one.  See Kripke and others on
the topic of Naming and Necessity.

Were Rosa Parks still around she would surely not judge equality evil.


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

Re: Is equality evil?

[Toby Bartels]

Thomas Streicher wrote in small part (in a post about fibrations):

>Even in intensional type theory there is a notion of equality.

Elsewhere in the same thread, Vaughan Pratt wrote:

>Theorem.  Equality if and only if the diagonal.

and concluded that equality is no more or less evil than contraction.


This depends on what kind of type theory you are using!

In the intentional type theory of Martin-Loef, for example,
there is a notion of equality (or identity) at each type.
Heck, there's even a notion of identity of types!
However, one can certainly consider type theory without identity types.
I would suggest the internal language of a Heyting 2-pretopos
(although that depends on what one takes this language to be).

Logic should be the servant of intuition, not the master.
If some category theorists have the intuition (and we do)
that it is meaningless to speak of equality of objects,
then it's the job of the logician to find a formal language
which expresses only what these category theorists find meaningful.
If they haven't done so, then this is something to work on,
not an argument that the motivating intuitions are invalid.

There is something else that logic can do, however:
it can show that identity follows from something else.
Vaughn's theorem (cited above) purports to do this,
but it is based on the assumption that every operation between types
(in this case, the diagonal Delta_X: X -> X x X)
has (as "image" or "range") a predicate on the target type
(in this case, the identity predicate on X x X).
So if our intuition suggests that operations have ranges,
then we must accept that we have identity predicates too
(assuming that we can construct the diagonal operation using contraction).

But my intution suggests no such thing for arbitrary types
(such as might be suitable as the type of objects of a category);
naively, given an operation f: X -> Y, the range predicate (ran f) on Y
would hold at those objects of Y with the form f(a) for some object a of X.
But given an object b of Y, how do you determine if it has this form?
If we already had an identity predicate =_Y on Y, then we could do this:
(ran f)(b) if and only if (for some x: A) (b =_Y f(a)).
But in general, I don't see any meaning for the range of an operation.

In fact, since I'm happy to use contraction in general mathematics,
I would phrase Vaughn's theorem as follows:

>Theorem.  Equality if and only if ranges.

and conclude that equality is no more or less evil than ranges.
But I don't believe in either of these, in general;
that is, I believe in the usefulness of types that lack these.

(Quiz:  Given two arbitrary sets, say the set of natural numbers
and the set of positive integers, how do you decide if they are equal?
Similarly, given a set and an arbitrary operation on sets,
say the set of rational numbers and the operation of cartesian square,
how do you decide if the set belongs to the range of the operation?
Or more relevantly, given the diagonal operation on sets,
how do you decide if a pair of sets belongs to its range?)


--Toby


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

Re: Is equality evil?

[Thomas Streicher]

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

Re: Is equality evil?

[Erik Palmgren]

Thanks Thomas for bringing up the intensional type theory perspective. Here
equality of objects in categories is a serious problem already for sets,
or rather for their type theoretic counterpart, setoids (types with
equivalence classes). The so-called identity types give a minimal
equality on each type A: Id(A,a,b) are the proofs that a and b
are equal in A. But the fact that these proofs are in general not
unique and induces a groupoid structure makes it difficult to apply
when e.g. A is a universe of types. Some remarks are contained in
in this preprint

http://www.mittag-leffler.se/preprints/files/IML-0910f-36.pdf


If one tries to use the Id-types to define equality on (small) setoids
one ends up with a groupoid of objects rather than a setoid objects.
I think the situation can be described as follows for a general category K,
which we think of as a category without equality of objects. We now
want to induce an equality of objects on (a part of) K. Take a
groupoid G and a functor F:G -> K. We define the groupoids of
objects C_0, arrows C_1 and composable arrows C_2 in a natural
way. C_0 is G and C_1 has for objects triples (a,b,f) where a,b in G
and f:F(a) -> F(b), and a morphism (a,b,f) -> (a',b',f') is a pair of
G morphisms r:a -> a' and s:b -> b' with F(s) f = f' F(r). C_2 has for
objects pairs of morphisms composable with an mediating map m from G,
i.e. ((a,b,f),(c,d,g),m). The composition is g F(m)f. The morphisms of
C_2 are then pairs of C_1 morphisms

((r,s), (t,u)): ((a,b,f),(c,d,g),m) -> ((a',b',f'),(c',d',g'),m')

with m's= t m.

When G is a discrete groupoid this becomes a standard category. When G is
a groupoid it becomes almost a category. Notions of limits can be
formulated in a natural fashion. At least when K=Setoids, C inherits
limits from K. Perhaps some general results are known about this
construction of C from functor F:G -> K on a groupoid G?


Erik


> 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.
>

......

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

Re: Is equality evil?

[Bas Spitters]

> 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.

Vladimir Voevodsky just posted a draft manuscript about these issues:
http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html

Bas


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

Re: Is equality evil?

[Toby Bartels]

Thomas Streicher wrote in part:

>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.

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.
But I would not write any particular predicate into the language,
even with intensional behaviour, if I don't need it.

However, it is interesting that intentional identity types/predicates
satisfy weaker axioms than the extensional equality of first-order logic,
enough so that we are still driven away from using strict concepts.

>identity types are not necessary for doing constructive mathematics.

Nor for nonconstructive mathematics; excluded middle is a red herring.
Type theory naturally lends itself to constructive interpretation,
but one can add rules for excluded middle, even the axiom of choice,
if one wants to do classical mathematics.

However, questions of predicativity ARE important.
(Some type theories become impredicative when excluded middle is added,
  as Martin-Loef's do, but not all do; impredicativity is what matters.)
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.
(This definition is usually attributed to Gottfried Leibniz.)
So you get an identity predicate by quantifying over all predicates,
in a theory that allows this.

It would be interesting to hear from people who want to keep kosher,
but also want to reason impredicatively, how to interpret this definition.
(For my part, I want to be both kosher *and* predicative by default,
  only abandoning predicativity when this seems to be needed.
  Very little basic category theory relies on impredicative reasoning.)

>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.

Quite right; I really should not have mentioned that at all.
So everyone, delete this line from your memory of my previous post:
>>Heck, there's even a notion of identity of types!

Identity judgements are less problematic than identity types.
And some form of identity judgement seems to be necessary
to fully develop foundational-strength dependent type theory.
Actually, I don't so much seem to need identity judgements
as beta-convertibility (although you can define beta-equivalence
in terms of beta-convertibility, and call that identity).
I started to write this up once, but I never finished it.

The point is that one can recognise that two syntactic expressions,
such as x and x, are the same, or even that one reduces to another,
such as fst(x,y) and x (where fst: A x B -> A is the usual projection),
but this is different from taking two completely different expressions,
such as x and y, and considering the hypothesis that they are the same.


--Toby


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

Re: Is equality evil?

[Michael Shulman]

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

Re: Is equality evil?

[Thomas Streicher]

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