[FOM] Dual of a category

[Laurent Delattre]

> they are in one-one correspondence); consider, for
> example the Ph.D. 
> thesis "A Formal Calculus of Categories" of Mario
> Caccamo,  in which the 
> formalization of duality "...results in a
> nonstandard notion of 
> substitution of terms." The thesis is available
> online at 
> http://www.brics.dk/DS/03/7/.

I had a look at this thesis.
Caccamo defines a type system where terms are functors
and types are categories. He assumes the following
syntactic equalities on categories (i.e. types):

  C^op^op = C
  (C*D)^op = C^op * D^op
  [C.D]^op = [C^op, D^op]

I wonder if they could be replaced by typing rules. A
definition of C^op through Cat^op might do the
trick...



	

	
		
___________________________________________________________________________ 
Nouveau : téléphonez moins cher avec Yahoo! Messenger ! Découvez les tarifs exceptionnels pour appeler la France et l'international.
Téléchargez sur http://fr.messenger.yahoo.com