Currying of functors
Category of small categories is closed.
This means that we can apply curry on functors, eg.
(a⊗b → c) → (a → b → c)
However currying changes the meaning of a functor.
(a⊗b → c) means that if we send an object from
we'll get back an object from
Likewise if we send a morphism from
we'll get back a morphism from
(a → b → c) means that if we send an object from
we'll get a functor
(b → c). Whereas if we send a morphism from
we're going to get back a natural transformation
b → c.
To illustrate this change, lets consider a product functor.
c⊗c → c.
If we send an object from
c⊗c -category, it will produce a product.
We could define it as:
xy ⊢ (xy₀ * xy₁).
If we send a morphism from
c⊗c -category, we'll get a morphism.
That we could also define as:
fg ⊢ xy ⊢ (fg₀ xy₀, fg₁ xy₁).
The moment we curry the product functor, we'll get
c → c → c.
Now if we send an object
we're going to get a functor
c → c, which we can also define:
y ⊢ (a * y) and for morphisms:
g ⊢ xy ⊢ (xy₀, g xy₁).
However if we send a morphism
we're going to get a natural transformation
c → c.
(a * -) → (b * -). This can be also defined through a lambda:
λay. (f ay₀, ay₁).
Cat -category is cartesian closed means
that we can compose functors with lambda calculus,
but it obtains this extra meaning when we apply the resulting functor
to objects or morphisms.
Here's an interesting case to consider.
Both initial and final fixed point retrieves an endofunctor.
The signature of fixed point constructor is:
(c → c) → c.
Now lets say we apply
λa. fix (λx. a*x). If we send an object,
the result is obvious: we get a fixed point -object with product functor.
How about we send a morphism?
The constructor for initial fixed point is
in, and destructor is
I guess that I'd get
f ⊢ cata (λay. in (f ay₀, ay₁)).