Freyd Categories

Freyd Categories

[David Leduc]

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/ ]

Re: Freyd Categories

[Paul Levy]

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/ ]

Re: Freyd Categories

[Toby Bartels]

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/ ]