TODO:
O. Think of the human intefrace
The program should be able to accept new rules (and record!)
during the search. These new rules represent what is known "externally"
about the underlaying category.
I. Implement diagram chasing in a Quillen model category
(with many morphisms):
HOWTO: Notice that a commutative diagram in a Quillen
model category is a quilder.
Thus, QuilDer-BuilDer maintains
a collection of quilders repsenesting commutative diagrams
already constructed. An application of
Rules I-III (the rules of lifting and wc-f and c-wf and co/limits)
adds a new quilder to the collection and then merges it in some of
the existing quilders.
It is rather uncler to to maintain the collection of quilders
efficiently.
II. Implement diagram chasing in a labelled poset with arbitrary rules.
III. Implement diagram chasing in an arbitrary caetgory using II and I.