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