So, we’re still working towards showing the relationship between linear logic and category theory. As I’ve already hinted, linear logic has something to do with certain monoidal categories. So today, we’ll get one step closer, by talking about just what kind of monoidal category. As I keep complaining, the problem with category theory is that anytime you want to do something interesting, you have to wade through a bunch of definitions to set up your structures. I’ll do my best to keep it short and sweet; as short as it is, it’ll probably take a bit of time to sink in.
First, we need a symmetry property. A monoidal category C (with terminal object t, tensor ⊗, and natural isomorphisms λ, ρ) is *symmetric* if/f for all objects a and b in C, there is a natural isomorphism γa,b : (a ⊗ b) → (b ⊗ a); and the categories monoidal natural isomorphism ρ = λb º γb,t : (b ⊗ t) → b.
In other words, if you reverse the arrows, but leave everything else the same, you still wind up with a monoidal category.
In a similar vein: regular functors are also sometimes called *covariant* functors. If you take a functor and *reverse* the directions of all the arrows, you get what’s known an a *contravariant* functor, or *cofunctor*.
We also need a *closure* property. Suppose C is a symmetric monoidal category. C is *monoidally closed* if/f there is a functor ⇒ : C × C → C, such that for every object b in C, there is an isomorphism Λ : (a⊗b → c) → (a → (b ⇒ c)), and Λ is a natural transformation for a and c. (Remember that a and c are categories here; this is a natural transformation from category to category.)
Basically, this just says that the tensor stays cleanly in the monoid, and there’s always a natural transformation corresponding to any use of tensor.
So what these two really do is pull up some of the basic category properties (closure with respect to composition, symmetry) and apply them to categories and natural transformations themselves.
Finally, we need to be able to talk about what it means for a *functor* to be closed. So suppose we have a monoidally closed category, with the usual components, up to and including the Λ natural transformation. A functor F : C → C is *closed* if, for all a,b in C, there is an arrow fa,b : ba → F(b)F(a) such that for all g : a → b, fa,b º Λ(gº λa) = Λ(F(g) º λF(a)).
In simple english, what a closed functor is is a functor that can be *represented by* an arrow in the category itself. That’s what all of that gobbledygook really means.
So… as a quick preview, to give you an idea of why we just waded through all of this gunk: if you take a monoidally closed category of the appropriate type, then collections of resources are going to be categories; ⊗ is the tensor to join collections of resources; and “-o” implications are the closed functors “⇒”.
Good Math/Bad Math
The beauty of math; the humor of stupidity.
I don’t think cofunctor is standard. Functors come in two types contravariant ( what you called cofunctor) and covariant (what you called functor). A contravariant functor is a functor from the opposite category.
If C is a category the opposite of C, C^{op} is the category with the same objects, but with all the arrows turned around.
That is if A,B in C then Hom_{C^{op}}(A,B) = Hom_C(B,A)
The opposite category is one of the more useful ideas in Category theory. For example if C is an abelian category then so is C^op. (Abelian means that Hom(A,B) is an abelian group among other things)
This allows dualizing proofs.
Kernels products, and limits correspond to Cokernels coproducts colimits in the opposite category and visa verse.
So for example a theorem about limits becomes a theorem about colimits, provide the opposite category also satisfies the hypothesis of the theorem.
elspi:
Unless I’m seriously mis-remembering something, there’s a reason why the functors and the cofunctors are different. The cofunctors are functors in the dual category, but with respect to the category that you’re looking at, contravariant functors are *not* functors, in that they do not respect composition rules correctly. Covariant functors, aka “normal” functors, are the ones that are “well-behaved” with respect to the morphisms in the category and compositions.
yeh
A contravariant functor is a convarient functor with “domain” the oposite category. That is $f: C->D $ is contravariant means that $f:C^{op} ->D$ is a covarariant functor.
In standard usage, functor means both covariant and contravariant.
WARING: I am not a Category theorist, I just am forced to do homological algebra now and then.