Related work
It's curious when you start to explore some mathematic field, and when you finally find the appropriate categorical terms for expressing your ideas, and try to Google those ideas, you always find a two year old free online book describing almost exactly what you have found, but in a slightly different field. I guess that's the beauty of using CT as an interlingua for mathematics. I think there are still some holes for me to fill in, but it seems I won't have to do a lot of the math. Polynomial Functors: A General Theory of Interaction by David I. Spivak and Nelson Niu I have also found an early attempt to make a more formal definition of lambda calculus in categories that allows them (Cartesian Closed Categories have all finite exponential objects). https://golem.ph.utexas.edu/category/2006/08/cartesian_closed_categories_an_1.html