more on monoidal structure of graphs

[Francois Lamarche <Francois.Lamarche@loria.fr>]

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