Computer algebra system for category theory

Question

There are many different computer algebra systems which allows to perform computer aided computation in symbolic object like polynomials and function and also ordinals. Now being a category theory fanatic I'm wondering if there's any such system which can perform calculation in any 2-category. So.......

does anyone know a computer algebra system which can perform calculation with 2-categories and or string diagrams?

Answer 1

Pretty sure it is not exactly what you're looking for, but Sage is designed in an categorical way (for instance, a group is an instance of the subclass Groups of the class Monoids, which is in turn a subclass of the class Magmas, etc.), and so has some features related to category theory.

Answer 2

Maybe it's better that I answer this question, since I posed it to ineff yesterday. I let him ask the question since he is definitely more keen on the subject :) the following explanation is the best I was able to write. Sorry if it seems (and in fact it is) the product of a really simple-minded programmer!

What I had in mind was to write down a simple (?) program helping me to avoid embarassingly elementary questions like this, which turn out to be blatantly trivial once you drew the right diagram.

But now suppose that diagrams can't help you (e.g. suppose they become really huge), and you can only trust bare computations. You have to check whether

{something complicated} = {something even more complicated},

or you wrote "1" in a really complicated fashion and you want to "reduce" it in a suitable sense, with respect to some suitable algebraic laws[2].

Now what I want is to define a "type" Object and a "type" (or a structure? I don't remember almost anything about these topics :) ) Arrow (or 1-cell), where an "arrow" consists of a triple {D,C,f}, where $D,C$ are objects, the domain and codomain of the arrow $f$[3]. The collection of 1-cells come equipped with two (in fact, three) maps Object source(Arrow f), Object target(Arrow f) and int Name(Arrow f), doing what you expect they do. Arrows can be composed if the domain of the one coincides with the codomain of the other (and I think that the problem reduces to the implementation of this operation and the definition of its rules -label a special arrow as the identity, how do you cope with commutative-square-like situations?).

A 2-cell consists now of a square $$ \begin{array}{ccc} A &\to&B \\ \downarrow&\alpha&\downarrow\\ C&\to & D \end{array} $$ having horizontal and vertical source and target:

• The horizontal source of $\alpha$ is the arrow $A\to C$;
• The vertical source of $\alpha$ is the arrow $A\to B$;
• ...
• vertical and horizontal source and target are linked by suitable relations: $s(s_v(\alpha))=s(s_h(\alpha))$, $t(s_v(\alpha))=s(t_h(\alpha))$, etc.

Notice that "natural transformations" arise as those 2-cells having identity arrows as horizontal domain and codomain. I think the most naive way to describe a 2-cell is by an inductive argument (exploiting again internalization): $\alpha$ is a structure consisting of a 4-tuple of arrows, such that "they form a square": Arrow Vsource(Nat alpha), Arrow Hsource(Nat alpha), Arrow Vtarget(Nat alpha) and Arrow Htarget(Nat alpha) are given in such a way that the former relations are satisfied.

2-cells can now be composed horizontally ($\boxminus$) and vertically ($\circ$), and I would like to

• Define these compositions and impose the interchange law
• Recover the "whiskering" operation $\alpha*F$ of a 2-cell $\alpha$ and a 1-cell $F$ as horizontal composition of an identity two cell with another composable 2-cell
• Do computations! Suppose now you want to check without any graphical help whether $\theta\circ ((\alpha * F)\boxminus (\gamma\circ \beta)\boxminus (H* \delta))=$something. You feed your program with something like

Vcomp(theta , etc.)

you cross your fingers and then you hopefully get something you can more easily compare with what you desire (the identity 2-cell, an endomorphism of a suitable 1-cell, ...).

====

[2] yup, I know that computationally speaking I'm asking first to run for a km or two and then to climb the Karakorum, but let me get to the point.

[3] which is an element of a suitable alphabet: this is not minimal since I can deduce objects from identity arrows, but I feel more comfortable in this way. Suppose for example you are labeling arrows $A\to B$ with positive-integer labels

Answer 3

You can also try:

1. a GAP package called CAP, which is part of the homalg system.
2. Cateno

-- Mike