Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
GSoC 2012 Application Sergiu Ivanov: Category Theory Module
Clone this wiki locally
GSoC 2012 Application Sergiu Ivanov: Category Theory Module
Name: Sergiu Ivanov
Enrollment: University of the Academy of Science of Moldova, http://www.edu.asm.md/en (partly in Romanian)
scolobb, GitHub username:
My initial focus was on computer science; in the years 2004-2007, I have successfully taken part in a number of school Olympiads in programming and algorithms. At the university (2007-2011), I have studied formal languages, operating systems, networking, databases, object-oriented programming and Prolog. In my spare time I have got acquainted with a number of programming languages and frameworks, among which are C/C++, Java, Python, .NET/Mono, Smalltalk, Common Lisp, Haskell. At the university, I have also taken courses in calculus, probability, discrete mathematics, numerical methods, and optimisation.
In tried to be a part of GSoC 2008 with GNU/Hurd, with the project "Namespace-based Translator Selection". I was not accepted because of my low activity during the proposal ranking period; however, I worked on the idea voluntarily; one can find the short report of what has been done here. I was accepted to GSoC 2009 to the same organisation (GNU/Hurd), with the project "VFS-based Unionmount". The documentation of the tool I have developed (by extending another one) can be found here.
In my last year of bachelor studies I have implemented a remoting framework in Haskell. The code is here. My diploma project was a simulator of P systems written in Java, Jython, C, and Haskell. The code is here. In my diploma project I made use of OpenCL/CUDA.
I am currently pursuing MSc in "Mathematics and Informatics". I have had courses in parsing, theory of algorithms, measure theory. I have had (or am having) quite a bit of algebra-related courses: modules (and a bit of rings), lattices, quasigroups, Gröbner bases. I am doing part-time research in computability theory with focus on unconventional computing models. In my spare time I am learning category theory, functional programming, and lambda calculus.
My Environment and Coding Skills
I'm running the latest 64-bit Gentoo Linux. I have Python 2.7.2 installed. I prefer to code in Emacs.
I have been using Python every now and then for about 4 years now. I wrote simple to moderately complex university assignments in Python, including a wxPython-based application for creating and editing simple graphs and for running basic graph algorithms (minimal spanning trees and shortest paths mainly) with a custom widget for visually editing graphs. My knowledge of Python remains somewhat patchy, though.
Although I have had encounters with other version control systems, I am most comfortable with Git. I have been actively using Git since 2009, including for management of my university coding and documentation projects.
I have submitted a fix for for Issue 3106; the corresponding pull request has been merged into master.
I have also worked on Issue 2142; the corresponding pull request has not yet been merged, but will hopefully be soon.
Category theory is a relatively new domain of mathematics which arose in an attempt to generalise existing algebraic structures. Because of the novelty of the approaches used in this domain, the number of people applying it is only increasing slowly. On the other hand, there is no way yet to represent category theoretic reasoning in modern CAS. The goal of this project is making SymPy capable of both representing category theoretic reasoning and carrying out a part of category theoretic reasoning automatically, with main focus on deciding the commutativity of diagrams.
Category theory is a branch of mathematics which studies a wide range
of mathematical objects by formalising them as object and arrows .
Informally, a category is two collections (defined in a set theory
) a collection of objects and a collection of morphisms
(sometimes also referred to as arrows), which have a domain (origin)
and codomain (destination), which are objects. Objects may denoted
by capital letters:
B, etc., while morphism may be denoted by
g. A morphism
f with domain
B will be written as
The two collections in a category may be "very large", they can be as large as to include all possible sets, for example. In terms of the modern set theory, these collections are referred to as classes. The class of morphisms has a number of additional properties, among which are the following:
f:A->Bcan be composed with a morphism
g:B->Cto yield the morphism
for every object
Athere exists a morphisms
1_A:A->Asuch that, for any
1_A f = f, and, for any
g 1_A = g;
1_Ais called the identity morphism of
Given this informal definition of a category one can immediately say that, for example, all groups and their group homomorphisms form a category, similarly to rings with ring morphisms, modules with module morphism, etc. However, the definition of a category turned out to be sufficiently general to cover not only collections of algebraic structures, but also a lot of other constructions. For further details, see the modern bible of category theory: .
One important thing that must not go unremarked is the fact that the objects of a category are not explicitly defined to have any structure; rather, their structure is revealed by studying their behaviour with respect to morphisms. Sometimes, however, information about objects is required, in this case one defines a concrete category A over a category B. For example, the category of groups and group homomorphisms is a concrete category over the category of sets. In contrast, categories which are not concrete are sometimes referred to as abstract categories.
One of the most important tools in category theoretical reasoning is
the commutative diagram. A diagram in a category A is a
subclass of objects and some of the morphisms between the objects.
For example, the objects
A,B,C\in A and the morphisms
g:B->C form a diagram. A popular way to represent such
diagrams is by actually drawing the objects as dots and the
corresponding morphisms as arrows between them. For example,  is a
graphical representation of a diagram. When drawing diagrams, it is
common to omit the arrows which are compositions of other arrows
already present in the diagram and which do not bear any special
significance for the diagram itself.
For further examples of (larger) commutative diagram, check out .
Consider a diagram in a category A and two objects
A which are connected by a path from
B in the diagram.
When one follows the path, one constructs the composition of the
morphisms represented by the corresponding arrows, in the order of
traversal. Thus, by following the path from
B in the diagram
A-(f)->C-(g)->B, one constructs the morphism
gf. A commutative
diagram is a diagram in which the following holds: for a pair
of objects in this diagram, every path from
B yields the same
It turns out that the property of a diagram to be commutative is sufficiently eloquent to express almost any category theoretic statements; this makes commutative diagrams one of the fundamentally important instruments in category theory. A lot of proofs are done by (or can be reduced to) checking whether a certain diagram is (or certain diagrams are) commutative.
In certain concrete categories, checking the commutativity of a
diagram can be done directly, by choosing an arbitrary element of the
A and computing to what element it is mapped in
B by every
B in the diagram. If the mappings are the same for
any such pair of objects
B, then diagram is commutative.
This approach obviously depends heavily on knowing the internal
structure of objects and the exact effect of every morphism in the
diagram. Thus, this approach will not obviously work for abstract
categories; in fact, it will not work for all concrete categories
even, in the cases when the structure of objects is insufficiently
The most general approach to checking the commutativity of diagrams is
based on the fact that a lot of category theoretical statements can be
expressed as the property of a diagram to be commutative. Consider a
category A with a set of properties expressed as a set of
D. Then a diagram in category A will be
commutative if it is a "composite" of some diagrams in
more formally, a diagram will be commutative if one can find
embeddings of diagrams from
D which are sufficiently "well-placed".
No software implementation of anything closely related to category theory currently shows up in searches. While tools for manipulating concrete algebraic structures abound, it seems that it is impossible to even represent category theoretical reasoning in any of the modern CAS. While not being a formally concrete source,  illustrates the situation rather vividly.
There have been some indications that people are working on having such things implemented, namely that a group of people on the
sage-combinat mailing list are creating a class structure similar to what I suggest. I will contact them to compare the scopes of our projects and see how we could do each other benefit.
This Google Summer of Code 2012 project has two major goals:
make it possible to represent category theoretical reasoning in SymPy by creating and manipulating categories and diagrams, and
make it possible to decide the commutativity of diagrams.
Relevance and Benefits for SymPy
While I believe that it is absolutely clear which benefits this project will bring to the end users working with category theory, the number of such users is still apparently very low. Therefore, I feel it necessary to explicitly elucidate the benefits SymPy herself will gain from having a category theory module. There are three fundamental points to this matter, as I see it:
Organisation of algebraic structures. Efforts are beginning to have SymPy deal with algebraic structures like groups, modules, rings. This makes the problem of having common fundamental infrastructure relevant. The category theory module will offer a number of classes which will serve as a checklist when implementing a new algebraic structure (homomorphism, zero object, kernel, etc.) and will contribute to uniform implementations of such structures.
Stating facts about algebraic structures. My implementation of diagrams will make it possible to state some facts about certain constructions (see, for example, Aaron's question about expressing isomorphisms between two groups ) and then effectively apply these statements by deciding commutativity of some other diagrams. Moreover, some category theoretic notions (functors ) will eventually make it possible to state more general facts involving heterogeneous algebraic structures (like the fact that a module has the underlying abelian group).
Priority. SymPy may become the first widely available general purpose CAS offering category theoretic tools.
Automatic drawing of commutative diagrams. People will be able to have diagrams typeset for them automatically, which is going to be very useful for authors of articles on category theory.
Please note that, while dealing with commutative diagrams involves working with graphs, commutative diagrams are a very special kind of graphs and, as I describe my vision of the implementation, it will be easy to notice that the whole thing includes much more details pertaining to mathematical logic and artificial intelligence (like backward chaining) than to graph theory.
I am going to split the implementation of this project into three mandatory phases, as well as an extra phase which is concerned with further improvement and extension of what will be implemented during the first three phases. Note that, due to the complexity of the things I will have to implement, I expect to only have the basics of the category theory module done by the end of the summer of code.
In this phase I will implement the foundation classes for representing the mathematical notions I have introduced earlier in the proposal.
I will start with defining the class
Class, which will represent a
class in set theoretic sense. Since the existing class
sympy.core is defined sufficiently loosely, I will leave
and essentially a synonym of
Set. This is done in the waiting for
the future implementation of set theory with distinction between
classes and sets.
I will then define
Object which will represent an object in a
Morphism, which will represent a morphism. In this
very basic form,
Object will only store a string name.
will store a name as well, but also a reference to the domain and
Morphism will also store a list
Morphism, which will initially be equal to
Morphism will have a method
compose() which will take a
as an argument and will return the morphism resulting from the
self and the argument, in this order, if the two
morphisms are composabable (
self has the domain equal to the
codomain of the argument). This new morphism will store references to
the morphisms it was obtained from in
functionality will be generalised for morphisms which are already
composites of other morphisms.
Morphism will also have a method
flatten() which will discard the information about compositions and
Next I will define
Category to contain an instance of
will represent the class of objects in the category.
have a method
morphisms() which will return the set of morphisms
between two objects belonging to the category. I will also define the
all_morphisms() which should return the class of all
morphisms of this category and will initially have it throw a
NotImplementedError. Note that it should not be required to
actually generate all morphisms of a category to construct the class
of all morphisms; I intend to only have a number of criteria which
will allow checking whether a morphism belongs to a
Category or not.
Category will also have a string field holding a name.
The next class is
Diagram, which will contain a collection of
objects of a category and the corresponding morphisms. In practise,
diagrams are often used to represent implications of the type "If
there are morphisms with such properties, then there also exist
morphisms with such properties and the diagram is commutative". To
cope with this, I will split the collection of morphisms in
into two parts: one representing condition of the implication and the
second part representing the result of the implication. Morphisms
will be stored together with their attributes, which will be
represented as strings ("unique", "exists", "isomorphism", etc.).
I will enable
Category to store a collection of diagrams which are
known to be commutative in this certain category and thus represent
the properties of this category. For convenience, the user will be
able to add a diagram to this collection by invoking the method
At the end of this phase I expect to have a basic, yet sufficient collection of utilities to represent a wide gamma of category theoretic reasoning limited to a single category.
In this phase I will focus on graphically representing diagrams. The reason for doing this so early is that visually apprehending a diagram is much easier than understanding the corresponding morphism equalities.
While a diagram can be perceived as a graph, there are a number of specific requirements to their graphical representation (take a look at ):
objects are represented as object names rather than points;
diagrams are most often represented in a grid-like layout;
morphisms which are compositions of other morphisms in the diagram are often omitted if they do not carry any useful properties.
I will start by adding the method
simplify() to the diagram. This
method will omit the morphisms which are compositions of other
morphisms shown in the diagram and which do not have any attributes.
I will then add the class
DiagramDrawer which will have the methods
draw_as_image() which will both take a
Diagram as an argument. The first one should produce a textual
representation of the diagram, while the second one should produce an
actual image. Both methods will throw a
DiagramDrawer. I will then define the class
draw_as_text() method to produce the TikZ code of the
image of the diagram. TikZ is a LaTeX package for creating graphics
Producing TikZ output offers a number of advantages, among which is that the resulting figure will be easy to include in LaTeX source and scale to the necessary size. Moreover, TikZ output will keep SymPy independent of any external library, while also allowing proper formatting of mathematical text using LaTeX expressions.
Eventually, the class
DiagramDrawer may be extended by a different
class which will be able to produce a graphical representation of a
diagram in a separate window, just like
Plot does currently. In the
meantime, it should be possible to achieve a similar effect by
wrapping the TikZ code from
TikZDrawer into a valid LaTeX skeleton
code, render it to PDF and show the result.
I will now present the idea of how to draw a commutative diagram. As I have already remarked, due to the specificity of the task, general algorithms are not applicable (at least not that readily). Remember that, in the end, we would like to see the diagram drawn in a grid-like layout. Another important remark is that we assume that the diagram is commutative.
Quite naturally, the process of representing a commutative diagram
graphically splits into two stages: the analysis stage, at which the
structure of the diagram is analysed and general decisions are taken,
and the drawing stage, which consists in actually producing text and
arrows. The analysis stage will be implemented as a set of methods in
DiagramAnalyzer. This class will include the method
draw() which will perform analysis of the supplied diagram and will
use an instance of a class derived from
actually do the drawing.
DiagramDrawingBackend will deal with the
technicalities of drawing and will expose a number of high-level
specialised methods, among which should be
draw_morphism_curved(), which will draw arced morphism to account
for the cases when the morphisms
A-(f)->B-(g)->C will get arranged
in a line and the a morphism
A-(gf)->C will also need to be
represented. Note that it will be the responsibility of
draw_morphism() to also draw the names of the objects and morphism
labels. Classes derived from
DiagramDrawingBackend will deal with
concrete back-ends; in this project I plan to implement
Drawing starts with the simplified version of the diagram, as returned
Diagram.simplify(). Then one step of constructing the
transitive closure of the underlying directed graph of the diagram is
performed. Note that, during the actual drawing phase, the morphisms
obtained at this stage will not be represented. After this
operation the diagram will consist of two types of structures:
triangles, consisting of triples of objects
Cwith the corresponding morphisms
pairs of objects
Band the corresponding morphism
The next stage is computing the "length" of morphisms included in the
diagram. Consider a morphism
f:A->B. If there are morphisms
k:C->B, then the length of
f is the length of
plus the length of
The actual drawing starts with choosing a minimal triangle (with
minimal sum of lengths of its sides). This triangle will be drawn as
a right-angled triangle. Then, for each side of the triangle, among
the list of all triangles which also include this side, choose the
minimal and draw it. This process will continue recursively while
there are no more undrawn objects which belong to a triangle. When
this happens, the remaining pairs of objects
B will be
drawn. For the cases when an object in this pair belongs to an "outer
rim" in the already drawn structure (i.e., in at least one of the four
directions "up", "left", "down", "right" nothing is yet drawn), the
morphism is drawn in one of the free directions. For the remaining
pairs, the objects which are yet to be drawn will be arranged in a
circle around the already drawn structure.
For each of the yet undrawn morphisms, check if this morphism goes
horizontally, vertically, or diagonally (
k*pi/4 relatively to the
horizon). If so, draw the morphism in an arc; if not, draw it in a
Note that, except for the last stage of placing objects, when they are arranged in a circle, all objects get placed in a grid. Besides being in agreement with the initial requirement, this will also allow the drawing algorithm to remember where the objects are placed by storing a rectangular array of flags. This array is how the algorithm will know whether an object is on the "outer rim".
At the moment, the behaviour of the drawing algorithm for a wrongly constructed diagram with more than one connected component is undefined. It is easy to check for this problem, however, if this eventually proves necessary.
While the algorithm exposed in this section is definitely unfit for representing general graphs, I expect that, due to the specificity of the underlying graphs of commutative diagrams, it will work well. Note again that a normal size for a commutative diagram is under 20 objects, which will also allow deducing heuristics to further improve the drawing algorithm.
Deciding the Commutativity of Diagrams
In this phase I am going to implement the procedure for deciding
whether a diagram is commutative, provided that a certain set of
diagrams is commutative. Remember that
Category.assert_commutative() is used to explicitly state whether a
diagram is commutative in a certain category.
Checking the commutativity of a diagram will be initiated by a call to
Diagram.is_commutative() which will take as argument a list of
diagrams which are known to be commutative or a
Category in which
the check should be performed. In the following paragraph I will
describe the actual functionality without going into detail as far as
splitting the code into functions or methods is concerned. The reason
for not doing this is that I consider that how this separation is
going to happen is rather obvious.
I will start the presentation of the procedure by remarking the similarity between deciding the commutativity of a diagram and an inference problem in artificial intelligence . Indeed, we start from a number of facts (diagrams known to be commutative) and we need to arrive at a certain goal (whether a certain diagram is commutative). One of the most widely used approaches to practically solving such inference problems (especially for non-zero-order logic) is backward chaining . I will show how backward chaining can be directly adapted to decide the commutativity of a diagram.
Backward chaining is a recursive procedure which starts from a given
goal and tries to unify  the goal with one of the available
predicates. A recursive step can be viewed as consisting of two
stages: the pattern matching  stage, at which the predicate to
unify the goal with is chosen, and the unification stage, at which the
unification itself is performed. For every matching predicate and the
result of unifying the goal with it, the procedure is repeated
(recursively). A parallel can be informally built with the
commutativity problem. Take the target diagram as goal and the
diagrams commutative known to be commutative, as known predicates
(facts, actually). The pattern matching stage consists in finding the
diagrams which "fit" into the target diagram. The unification stage
consists in adding the "necessary" (see definition of
morphisms to the target diagram and in marking the resulting
"subdiagram" as commutative. The procedure is recursively restarted
for any such match and goes on until a branch of recursion "proves"
that the whole target diagram is commutative or until all branches end
up with a negative result.
I will now give a technically detailed description of the algorithm, structured in blocks, according to the overview in the previous paragraph.
The algorithm starts by constructing the reflexive and transitive
closure of the target diagram. On the other hand, it will
simplify() each of the diagrams known to be commutative. This will
be done with the hope to improve performance.
Recall that a
Diagram includes two sets of morphisms, one of which
corresponds to the premises of an implication, while the other one
represents the result of the implication. The pattern matching
stage consists in finding an embedding of the underlying directed
graph of the premises of a diagram
D_1 known to be commutative into
the underlying directed graph of the target diagram. Note that
morphisms in a
Diagram possess attributes, which will be considered
when looking for an embedding. Thus, an embedding of
D_1 will only
be chosen for unification if all the morphisms in the embedding have
exactly the same sets of attributes as the corresponding morphisms in
The unification stage will consist in adding the morphisms of
which represent the result of the implication to the target diagram
and in marking the obtained subdiagram (essentially, a subgraph of the
underlying graph of the target diagram) as commutative by annotating
each morphism in the subdiagram with the same commutative component ID
(number). If the new commutative component has common edges
(morphisms) with another commutative component, then these components
are merged into one by annotating their edges with the same component
After unification, the procedure continues recursively. If no embeddings were found, a negative result is returned. If at least some of the recursive calls returns a positive result, this result is immediately propagated up the recursion tree. Note that, since unification may add new morphisms, at each new recursive call, one must examine all diagrams known to be commutative anew, regardless of whether either of this diagrams has already been unified with.
Positive result is obtained when the whole diagram is proved to be a single commutative component. This can be verified by checking whether all morphisms have been marked with the same connected component ID. This check will happen at the beginning of each recursive call, right before pattern matching.
Further Benchmarking, Optimisations and Extensions
As I have said in the introductory paragraph, this phase is optional and I will only manage to enter it if I complete the previous stages sufficiently soon. I would like to note, however, that I will continue working on the items enumerated in this section after the end of the Google Summer of Code program.
The following represents a list of things which will receive special attention during this phase (in no particular order):
Benchmarking and optimisation. The algorithms I have described in the previous sections will need to perform rather demanding computations. I expect that performance will be acceptable due to the relatively small sizes of practical commutative diagrams, but this has to be thoroughly verified. While doing the benchmarking, I also expect to collect sufficient understanding of how performance depends on input data in order to develop better heuristics and optimise further optimise the algorithms.
Showing resulting embeddings. I suppose that it will be useful to actually see the embeddings which led to deciding that a diagram is commutative. This should be rather easy to implement.
Rendering the diagrams. This will be implemented by wrapping the TikZ output from
TikZDrawerinto skeleton LaTeX code, rendering the code and popping a PDF viewer window with the rendered diagram.
Integration with implementations of group theory. In this summer I expect to see group theory implemented in SymPy. It would be very illustrative to actually integrate this implementation with the classes described in section Class Hierarchy. Moreover, it may provide some very useful practical insight which may contribute to certain modifications of the class hierarchy I plan to implement initially.
Non-technical documentation. While I absolutely will write rather detailed docstrings for anything I will implement, separate user-friendly and non-technical documentation with a proper outline is always better, and this is what I am going to provide.
The following list summarises the results I plan on obtaining by the end of summer:
a basic class hierarchy for representing category theoretical reasoning within a single category,
functionality to graphically represent commutative diagrams, and
functionality to automatically check for commutativity of a diagram starting from a set of diagrams known to be commutative.
Why I Fit
I have been rather intensively studying category theory for about 6 months already (with a slight interruption in the latest month). I have olympiad experience with solving problems on graphs and I have read . I do have what I consider solid (but not exhaustive) experience with Prolog and I have coauthored a paper on doing forward and backward chaining with P systems (a biologically-inspired computational device) . I believe this makes me well-equipped for solving the problems I have posed in this proposal.
Before the start of the coding period, I will have to spend quite a lot of time on university matters, which leaves about 2-3 hours per day for SymPy. In this time I plan to rebase https://github.com/sympy/sympy/pull/563 , as well as to work on http://code.google.com/p/sympy/issues/detail?id=2528 I will also continue studying . Further, I will throw a look at how different graph packages draw graphs (for example, I will scan the code of the functions listed in ).
The schedule of the summer exam session has not yet been firmly established at my university; it is absolutely certain, however, that I will have finished all my exams by June 1st. While I expect to have finished earlier than that, I will plan my activities starting with this date.
During the period before mid-term evaluations, I plan to be fully dedicated to the project, which amounts to not less than 7 hours on average, every day (including the weekend). After the mid-term evaluations, closer to the end of July, I may leave for a week of vacation. Aside from that, I am going to spend the same amount of time (7 hours every day) working on the project.
The following is an approximate timeline of my activities at week scale:
June 1 - June 3: start creating the class hierarchy, write some basic test suites;
June 4 - June 10: finalise the classes started the previous week and extend the test suites;
June 11 - June 17: implement
Diagram.simplify()and create the skeletons of classes pertaining to drawing the diagrams; write the test suites;
June 18 - June 24: implement
June 25 - July 1: implement the core of the drawing functionality;
July 2 - July 8: finalise the drawing functionality; improve the heuristics;
July 9 - July 15: write the tests for the procedure of deciding the commutativity of a diagram; implement the pattern matching stage; start working on unification;
July 16 - July 22: implement unification;
July 23 - July 29: polish and finalise the code; start doing benchmarks and improving the heuristics;
July 30 - August 5: write non-technical documentation; implement showing the embeddings which resulted in deciding that a certain diagram is commutative;
July 6 - August 12: integrate the (already done) implementation of group theory with the category theoretic classes;
August 13 - August 19: sort out the remaining issues; start working on a direction enumerated in the next section.
Note that, while I do not explicitly remark this in the timeline, I expect to be pushing the changes upstream as soon as I have bits of functionality which I am confident in. This will hopefully keep the burden of reviewing the changes low.
After the end of GSoC-2012 I plan to finish the tasks listed in the fourth stage of the implementation, but also work on other problems listed in the following section.
While the amount of work I plan for in this project is rather big, it will only lay the foundations of a proper implementation of category theory in SymPy. Among the things which should eventually be implemented are the following (in no particular order):
Functors . Category theory is said to have three notions at its foundation: category, functor, and natural transformation (functor morphism). Implementation of only one of these three notions is planned in this project. Implementing the other two will make the category theory module considerably more suited for much a larger class of practical problems.
Better diagram drawing. I do not expect to arrive at absolutely flawless drawing functionality at the end this summer. There is yet a lot of experience to be gathered by solving practical drawing problems and understanding the specificity of the underlying graphs of commutative diagrams which influence the ways of representing them graphically.
Complex attributes in diagrams. It may turn out that simple string attributes for morphisms in commutative diagrams will not suffice for some particular cases. This will require introducing more complex attributes which will certainly influence the course of deciding the commutativity of a diagrams.
Direct verification of commutativity. Should the user have a concrete category with sufficiently detailed information about the structure of objects, it should be useful to be able to check the commutativity of the diagram directly, by symbolically computing the mappings of elements along paths in the diagram.
Diagram chasing. Directly verifying the commutativity of a diagram as described in the previous item is only possible when all the morphisms in the diagram are exactly known. This only covers a rather small subset of situations, which is why it would be very useful to eventually implement diagram chasing.  may be helpful in achieving this goal.
 S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag New York Heidelberg Berlin, 1971.
 J. Adámek, H. Herrlich, G. E. Strecker. Abstract and Concrete Categories The Joy of Cats. http://katmat.math.uni-bremen.de/acc/acc.pdf
 R. Sedgewick, Algorithms in C++ Part 5: Graph Algorithms (3rd Edition) (Pt.5), Addison-Wesley, 2002.
 S. Ivanov, A. Alhazov, V. Rogojin, M. A. Gutiérrez-Naranjo: Forward and Backward Chaining with P Systems. IJNCR 2(2): 56-66 (2011).