Hi, A Freyd category is essentially a functor. So why is it called a category?! More generally, is there a way to see a functor as being a category? [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 23 Sep 2010, at 12:01, David Leduc wrote:
A Freyd category is essentially a functor.
That's right. It's neither a category nor due to Freyd.
So why is it called a category?!
I think there were two reasons. Firstly to portray the category of computations as being more important than the category of values. Secondly because an identity-on-objects functor between two categories with the same objects can be regarded as an [ -> , Set ] enriched category. Here -> is the category with two objects and a morphism between them (and identities). This point is emphasized in John Power's paper "Premonoidal categories as categories with algebraic structure" in TCS in 2002. Paul -- Paul Blain Levy School of Computer Science, University of Birmingham +44 (0)121 414 4792 http://www.cs.bham.ac.uk/~pbl [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
David Leduc wrote:
A Freyd category is essentially a functor. So why is it called a category?!
As I understand it, one says a Freyd category on C, where C is the source/domain of the functor. So a Freyd category on C is a category K (with certain structure), together with a functor C -> K (with certain properties). More simply, a Freyd category on C is a category K together with certain extra stuff. Calling that whole business (a category together with ...) a "category" is an abuse of language akin to terms like "partially ordered set"; a partially ordered set is really a set together with certain structure. There may be a better reason why Power and Thielecke used this terminology, but if so, they don't explain it in the papers that I have found (but I have not been able to read their first paper on the subject, Environments, Continuation Semantics and Indexed Categories, so maybe there is an explanation there).
More generally, is there a way to see a functor as being a category?
More generally, a functor is a pair of categories equipped with extra stuff, which is trivial, but I don't think that there's anything deeper than that. You could do something like the trick that encodes a function as a set (as everything must be) in the foundation of material set theory: a function f: X -> Y is the set {(a,b) in X x Y | f(a) = b}. But this set is isomorphic, in the cateory of sets, to X itself, so really we need this set together with maps from it to X and Y. Similarly, think of a functor F: X -> Y as the category with {(a,b) in Ob X x Ob Y | F(a) = b} as set of objects and Hom((a,b), (c,d)) := {(f,g) in X(a,c) x Y(b,d) | F(f) = g}, with the obvious composition; but again, this is isomorphic to X, so we really need it together with functors from it to X and Y. So I don't think that this really helps anything. --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (3)
-
David Leduc -
Paul Levy -
Toby Bartels