All Questions

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 ...

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 ...

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 ...

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 ...

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 ...