Since Michael's posting leapfrogged Marco's in the aether (at least from the viewpoint of our server) what I'll be saying may not appear in the right order threadwise to some. Marco Grandis wrote:
Would it not be simpler to work with REFLEXIVE GRAPHS and their cartesian closed structure? In my opinion, reflexive graphs are more natural than graphs:
The answer is no, because of the application in mind. We want to consider a graph as a constructive binary relation X(x,y), where an edge x-->y is a proof that (x,y) are related. We also want to build such things by induction, using universal properties. Reflexivity is often a desirable feature of the free structures you want to build, but you don't want it to come for free, since it creates redundancies and can mess up the induction principle associated with the structure. In certain situations you want reflexivity to be a consequence of the induction principle.
Remark 3. [The sequel is relevant for homotopy; I do not know if it may be relevant in CS, but I always had the impression that abstract homotopy should be of use there, eg with respect to deformations of processes, in some sense.]
There are two connections I know about between homotopy and computer science. The first has to do with process algebras, and originates in Eric Goubault's thesis, I think. Philippe Gaucher just sent a paper annoucement on this server about this line of research. The second connection is something Thomas Streicher, Martin Hoffmann and I discuss whenever we meet, which is not often enough. In constructive type theory there is a gadget called the Martin-L"of intensional equality predicate, J(x,y). So this is a version of equality, where you have to name the proofs that x=y. It has very simple (but rather mysterious) introduction and elimination rules, which can be translated as a universal property in a kind of higher-order universal algebra, where arities can not only be seen as finite sets, but also as families of sets, and families of families of sets and so on. In particular, since everything is a type, you have a type/predicate of equality proofs between equality proofs, and so on. For example given proofs that x=y and y=z, you can construct a proof that x=z, and you can do this uniformly, getting a term/algorithm J(x,y)*J(y,z) --> J(x,z) (here the * means a fibered product over y). But you cannot show that this operation is itself associative, it is only associative at a higher order. Ah! some kind of multiple category is involved! But so far all attempts to use higher-order categories to describe those weird algebras have failed. It only works at level one: when you collapse all proofs of equality between proofs of equality you get that the predicate J(x,y) is a groupoid structure. But when you try to go to level 2 the ordinary 2- or bi- or lax- or whatever- categorical machinery fails. You realize that simplicial sets are a better paradigm/starting point, but we need simplicial sets with operations. BTW is anybody from G"oteborg reading this?
This is why I think that the basic 2-dimensional categorical setting for abstract homotopy should only treat such "reduced horizontal composition": arrows with cells, cells with arrows, but NOT cells with cells. Formally, it is again a category enriched over reflexive graphs, BUT wrt the following monoidal closed structure:
X tensor Y: - the subgraph of XxY whose arrows are pairs (a, b), where a or b is an identity;
[X, Y]: - vertices: the graph morphisms; - arrows: their transformations (without "diagonals").
Hm... the geometrical motivations for not having full composition(s) here might well be related to the logical ones I mentioned briefly above. Francois