Skip to main content

All Questions

Filter by
Sorted by
Tagged with
3 votes
1 answer
140 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 ...
Johan Thiborg-Ericson's user avatar
2 votes
1 answer
327 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 ...
C. Bednarz's user avatar
1 vote
0 answers
67 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 ...
Johan Thiborg-Ericson's user avatar
1 vote
0 answers
66 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 ...
Johan Thiborg-Ericson's user avatar
1 vote
0 answers
97 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 ...
FeralX's user avatar
  • 73