Lax Indexed Functors?

[categories <cat-dist@mta.ca>]

Date: Wed, 29 Jan 1997 18:58:44 +0100 (MET)
From: Alfio Martini <alfio@cs.tu-berlin.de>


At the moment we are investigating logical systems and their relations based
on the formal concepts of institution (Goguen/Burstall) and entailment
system/logic (Meseguer). For our analysis we found  appropriate to use
concepts like "lax indexed functors" thereby having in mind the
corresponding definitions for ordered categories in 
"Extending properties to categories of partial maps" from
Barry Jay [Jay90] (TR ECS-LFCS-90-107).


To give  an impression about what we are doing, 
I will give the definition
that turns out to be the adequate one for our purposes:

A lax indexed functor F from an indexed category C:IND->CAT to an indexed
category D:IND->CAT is given by  functors F(i):C(i)->D(i) for each i in
|IND| and by natural transformations  F(g):C(g);F(j)=>F(i);D(g):C(i)->D(j)
for each morphism g:i->j in IND such that the following compositionality
condition is satisfied for any g:i->j and h:j->k in IND:

   F(g;h) = (C(g);F(h))*(F(g);D(h)).

(We also need the other version where F(g) goes from F(i);D(g) to C(g);F(j).)


To get the right feeling and insight we have developed all necessary results
by ourselves. Especially we were interested in the generalization of the
Grothendieck construction to "lax indexed functors".

Now, before fixing these things in a technical report, were are looking for
corresponding references of work already done in this direction. Especially we
don't want to introduce new names for already known concepts. We need
some advice here...

Our observation is that we have essentially used for many concepts and
results the 2-categorical structure of CAT. Thus we strongly believe that
somebody has already defined and investigated "lax functors" and "lax
natural transformations" for 2-categories.


Thanks for any help.

With all best wishes,

Alfio Martini.