In orthodox category theory, there are objects
as well as
morphisms
; since each object is essentially synonymous with an identity
morphism (on
that object), it is possible to elide the objects themselves
and use identity morphisms as tokens for them. However, to faithfully represent
some orthodox categories, it remains necessary to tag each morphism with the
identities (as ciphers for objects) it comes from
and goes to
: for
example, the category Set (whose objects are sets, morphisms are functions
– tagged in the manner under discussion – under clean composition,
i.e. f&on;g is only defined if every output of g is an input of f) requires us
to distinguish (A:f:) and (B:f:) whenever A and B are distinct sets subsuming
(:x←x:f), the set of f's outputs; yet, as relations, (A:f:) and (B:f:) are
identical in this case. (A similar complication arises with transformations
between functors.) With such tagging, two morphisms may package the same
underlying function (or whatever) yet be deemed distinct by the category: it
will only compose two morphisms if the end-tag of the first matches the
start-tag of the second.
While you are welcome to use such packaging to simulate an orthodox category, and this will work, I chose not to impose such a constraint on categoric binary operators.
For a given categoric binary operator, *, the relation follow(*) on its operands encodes what * can combine; follow(*) relates a to b iff a*b is defined. In general, for any relation r, I define end-relations
on the right and left values (respectively) of r; the former relates x
to y if x is a right value and r relates z to x
implies r relates z to
y
(whence, in particular, y is also a right value). Each is manifestly
transitive and reflexive (because subsumes is); hence intersecting each with its
reverse yields an equivalence. The end-equivalences of follow(*) and the
end-relations that yield them will encode the objects
of our category and
a containment hierarchy among them.
Written by Eddy.