Re: Equality again

[Patrik Eklund <peklund@cs.umu.se>]

I may have missed some parts of the equality message exchange, but here 
a few lines from general equational programming point of view.

I believe it is always important to note where equality or its genetic 
siblings reside. As far as I understand we do category theory mostly over 
ZFC, so ZFC is a metalanguage for category theory. The equality for "the 
diagram commutes" is in ZFC, but the "equation" t1 = t2 involving two 
terms over a signature is more tricky. You might say it's an ordered pair 
(t1,t2), and that structure is in ZFC. The objective of rewriting is to 
find a substitution (Kleisli morphism) s so that s(t1)=s(t2). More 
precisely, the substitution is a morphism s : X -> TY, so you extend it to
Ts : TX -> TTY, and bring it to mu_Y o Ts : TX -> TY with the mu from the 
term monad. All this is done over Set, i.e. T is a monad over Set, and 
therefore TX and TY are sets in ZFC. So, the equality in mu o Ts(t1) = mu 
o Ts(t2) is the equality in ZFC. Incidently, Set is already here in 
question as Set covers only the one-sorted signatures case. Moving over to 
many-sorted signatures you need more.

However, you can use composed monads instead of T, and you don't have to 
be over Set, or its multisorted cousin. Even more so, is it really only 
about ordered pairs? In the end, we are looking for a substitution 
bringing that "possibly something else than just an ordered pair" to 
something close to a 'singleton', where the notion of 'singleton' then 
should reside mostly in the purely categorical language, rather than in 
only and exclusively in ZFC.

General logics (Meseguer, Goguen, Burstall et al) in a general monadic 
setting both for terms as well as sentences, invites to this thinking, 
even if admittedly the programing examples at this point, for the monadic 
extensions, are rather artificial.

Also note that syntactics has for quite a while been studied with respect 
to categorization, but semantics is mostly seen in the metalanguage of set 
theory. Doesn't have to be so? Cannot be so? We are obviously trying to 
complicate things as much as possible in syntactics, and when it comes to 
semantics, our semantics domains are mostly sets, and equality is like 
the emperor, changing clothes all the time.

Best regards,

Patrik



On Mon, 24 May 2010, Joyal, André wrote:

> Dear Colin,
>
> You wrote:
>
>> It is an interesting impulse in higher category theory to avoid
>> identity in favor of isomorphism on the level of objects, and to avoid
>> isomorphism in favor of equivalence on the level of categories.   But
>> so far as I know no one has yet articulated a way to avoid ever using
>> identity of objects and identity of categories.
>
> I love the equality symbol more than an isomorphism symbol,
> and an isomorphism symbol more than an equivalence symbol.
> I always try to use the equality symbol whenever possible.
> I often use the equality symbol for a canonical isomorphism.
> Is there a special symbol for canonical isomorphism? (as oppose
> to a plain isomorphism). I would love to write something like
>
>  A times (B times C) =' (A times B) times C
>
> André
>
>

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