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 a⊗b category,
we'll get back an object from c category.
Likewise if we send a morphism from a⊗b category,
we'll get back a morphism from c category.
(a → b → c) means that if we send an object from a category,
we'll get a functor (b → c). Whereas if we send a morphism from a category,
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 a from c -category,
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 f:a→b from c -category,
we're going to get a natural transformation c → c.
(a * -) → (b * -). This can be also defined through a lambda:
λay. (f ay₀, ay₁).
That the 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 cata.
I guess that I'd get f ⊢ cata (λay. in (f ay₀, ay₁)).