equality tricks

Category theory is not equational. Meaning, in category theory equality is not defined for objects. We can only state that two objects are isomorphic. Well, of course x == x, but that's it; we can't always know whether x == y or not.

Now, to check for an isomorphism, we need to verify whether f ∘ g == id and g ∘ f == id. So we need some kind of equality for arrows. But if we could compare idx and idy, it would mean we could check whether x == y or not. No such thing is generally available. Yes, f == g implies dom(f) == dom(g) and codom(f) == codom(g) - but this is not available, so two different arrows are not comparable either.

Comparability is only local, that is, given x and y, and a couple of arrows, f: x → y and g: x → y, we can check whether f == g or not - but not in general settings.

This is okay. Except that, imagine, you define categories as (directed) (multi-)graphs with composition and identities. In this case we somehow have to discard equality of graph nodes. This is weird. A graph theory is usually considered to be equational. A non-equational graph theory is something one has to deal with if graphs are taken as a supertheory for category theory.

Why does not it bother me. I am implementing categories (as graphs) in Scala. And since Scala is a Curry type language (that is, with subtyping), comparing, e.g. two graphs (or two categories) is probably not implementable without using .asInstanceOf. So, a prudent programmer has two choices: either use .asInstanceOf - like Scala library does for sets (with a rather obvious error), or totally discard equationality for graph nodes. And this is unusual. E.g. we won't be able to produce a set of graphs. Or a set of objects of a category. Kind of challenging. Kind of new.

а помните 22 января 1991-го?

Тогда взяли да отменили 50- и 100-рублевки внезапно. Ну как внезапно, для ширнармасс внезапно.

Я тогда вздохнул с облегчением - моя странная идея не держать ничего в рублях вполне оправдалась. 

on equality

in the structural set theories we describe here, it is not meaningful to ask whether two elements of two different sets are equal; only whether two elements of a given ambient set are equal