All Questions
Tagged with cartesian-closed-categories lambda-calculus
6
questions
0
votes
0
answers
21
views
For which categories can the Cartesian closedness of a category be described as a family of covariant functors?
The paper Functorial Polymorphism describes how parametric polymorphism can be described as dinatural transformations. It involves second order lambda calculus but my question is restricted to simply ...
3
votes
1
answer
110
views
Where can I learn about Cartesian closed functors between categories of simply typed lambda calculus?
I'll try to describe the subject I am looking for literature on, or concept names that I can Google.
For each $n \geq 1$, let $\mathbf{STLC}_n$ be the category where the objects are all simply typed ...
1
vote
0
answers
64
views
Does lambda polymorphism have some universal property?
To evaluate some typed lambda calculus applications, the type of the function might have to be "lifted" in order to match the type of the value it is applied to. For example, in the ...
1
vote
0
answers
60
views
Second order lambda calculus as dinatural transformations in some category of CCCs
Let $\textbf{CART}$ be a category where the objects are all Cartesian closed categories (henceforth shortened as CCC). Is there any way to define the arrows so that $\textbf{CART}$ itself becomes ...
1
vote
0
answers
87
views
Is Set complete for the free CCC/lambda calculus over a monoidal signature?
To be precise, given a monoidal signature $S$ (i.e, a set of generating objects $O$ and morphisms with source and target taken in the free monoid over $O$) , we can generate the free Cartesian closed ...
- 63
2
votes
1
answer
299
views
Substructural types, the lambda calculus, and CCCs
It's well known that the simply-typed lambda calculus corresponds to a cartesian closed category. How would substructural type systems be characterized in category theory?
For example, linear type ...
- 31