The Category of Lambda Calculus

I have no idea how this should be done, but I am pretty certain (right now) that it is the way forward. As described in my first post, (almost) all objects in the lambda category are exponential objects of each other. The (possibly Cartesian product) contravariant part denotes the input, and the covariant part denotes the (probably curried) output. In Set, the universal arrow of the exponential object denotes how a pair of function and input is related to the output. The trick is to do the same thing in the lambda category. Next we have to consider that the function object is lifted by a (possibly identity) natural transformation before it is applied to the input, as described in the previous post. I don't know how yet. It will probably make sense to define a category were objects are exponentials, points of the objects denote the current function of the application chain and arrows are a pairs of a natural transformation and an input object of the right signature fed to the evalua...

In my last post I proposed seeing lambda polymorphism as a bifunctor, but this notion seems tio weak. Lambda polymorfism really needs three inputs, but one of them doesn't seem to involve any data in the set sense, only type data, connecting the types. I've tried making this into a category that defined every possible input as an arrow to the right output, but it didn't turn out nicely.  Instead I'm thinking of turning lambda polymorphism into a natural transformation. This seems promising, because as we all know, a parametrically polymorphic function is always a natural transformation. I will only scetch an example. The Church numeral 4 is applied to the Church numeral 3. Without polymorphism, this would not be possible, because 4 expects a signature * -> * in its first argument, but 3 has signature (* -> *) -> * -> *. We solve this by going by a * -> * functor before we apply the 3.  The * -> * functor is super simple. It takes every signature S to a...

So, I’m trying to think about how to define a category for lambda calculus. I’m thinking of a category that has as objects all the lambda function signatures and as arrows “the set of all lambda functions” somehow related by the domain and codomain signature. I am not sure exactly how to define the arrows, but currently it is much like Set, so all objects (except * and possibly some initial and terminal objects) are exponential objects. To create the exponentials, products are needed, but they are merely cartesian products, and exponentials are defined using the curry-uncurry isomorphism, as in Set. Let S be a non product signature with n inputs of signatures  s1, s2, … , sn,  so that  S = s1 -> s2 -> … - > sn -> *.  and T another non-product signature. Then the homset Hom(T, S) is the set of all lambda functions of signature T -> s1 -> s2 -> … - > sn -> *. If S is a product UxV, the arrows are pairs of arrows  from Hom(T, U) and Hom(T...