categories - Category Theory list
 help / color / mirror / Atom feed
* Re: more on monoidal structure of graphs
@ 1999-03-19 15:03 Marco Grandis
  0 siblings, 0 replies; 2+ messages in thread
From: Marco Grandis @ 1999-03-19 15:03 UTC (permalink / raw)
  To: categories

Francois Lamarche wrote

>...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.


I wonder whether the notion of "h4-category" which I introduced for
abstract homotopy theory (see the references in my first reply) might be of
use for this.

It is a sort of "2-category vertically relaxed up to a 'shadow' of 3-cells"
(whereas bi-categories are horizontally relaxed up to invertible 2-cells).

To begin with, it is a category enriched over reflexive graphs in the sense
previously described: there is a reduced horizontal composition, of maps
with cells and cells with maps, which is strictly associative as far as
this makes sense.
There also are vertical identities, vertical involution and vertical
composition, which only satisfy the usual axioms up to an assigned
equivalence relation ("2-homotopy").
This approach is truncated at the level of usual (first-order) homotopies;
3-cells (homotopies of homotopies) only leave their 'shadow', as an
equivalence relation.

If you want to proceed further, my impression is that the relaxed
categorical machinery becomes too heavy (at least for my taste). However,
if your 2-cells (homotopies) can be represented

- by a cylinder functor  I,  as arrows  IX -> Y,
- or dually by a path functor  P,  as arrows  X -> PY,
     (or by both, forming an adjoint pair  I -| P)

as it happens for most "concrete" homotopy theories, then the powers of
such endofunctor and the clone of operations (natural transformations)
linking them, derived from the basic ones (faces, degeneracy,
concatenation, etc.), seem to give all what we need in any dimension.
This machinery of derived operations can be seen in a paper of mine

Categorically algebraic foundations for homotopical algebra, Appl. Categ.
Structures 5 (1997), 363-413,

but of course "abstract cylinder functors" go back, at least, to Kan; other
references can be found in the paper above.


Regards

Marco Grandis








^ permalink raw reply	[flat|nested] 2+ messages in thread

* more on monoidal structure of graphs
@ 1999-03-19 13:27 Francois Lamarche
  0 siblings, 0 replies; 2+ messages in thread
From: Francois Lamarche @ 1999-03-19 13:27 UTC (permalink / raw)
  To: categories, grandis

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



^ permalink raw reply	[flat|nested] 2+ messages in thread

end of thread, other threads:[~1999-03-19 15:03 UTC | newest]

Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
1999-03-19 15:03 more on monoidal structure of graphs Marco Grandis
  -- strict thread matches above, loose matches on Subject: below --
1999-03-19 13:27 Francois Lamarche

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).