<p>If simply typed lambda calculus corresponds to cartesian closed categories, what types of categories do other calculi in the lambda cube correspond to?</p>
<p><a href="https://en.m.wikipedia.org/wiki/Lambda_cube" rel="noreferrer">https://en.m.wikipedia.org/wiki/Lambda_cube</a></p>

CC BY-SA 4.0
2020-08-02T12:17:04.967Z
I think https://ncatlab.org/nlab/show/locally+cartesian+closed+category might be of interest to you. In the references it says that dependent type theory is the interal language of locally cartesian closed categories. Also there is a paper called "Categorical Semantics for Higher Order Polymorphic Lambda Calculus" which discussed categorial semantics of the polymorphic lambda calculus (System F), but I do not know enough to understand it.
Labbekak
CC BY-SA 4.0
2020-08-05T05:41:40.147Z
I'm not aware of an explicit formulation of such a cube, but Bart Jacobs [1] goes through various structures and axioms that can be required of fibrations that correspond to different type system. One might be able to assemble a cube from the chapter/sections and combinations thereof.  [1] B. Jacobs, Categorical Logic and Type Theory. Amsterdam: North Holland, 1999.
Henning Basold
<lambda-calculus><ct.category-theory><dependent-type><typed-lambda-calculus>
Category theory lambda cube?
Eric Bond
# Category theory lambda cube?

(Asked by: username_0 on 2020-08-01)

If simply typed lambda calculus corresponds to cartesian closed categories, what types of categories do other calculi in the lambda cube correspond to?

<https://en.m.wikipedia.org/wiki/Lambda_cube>

**Tags:** lambda-calculus, ct.category-theory, dependent-type, typed-lambda-calculus

> **Comments:**
> **username_1**: I think https://ncatlab.org/nlab/show/locally+cartesian+closed+category might be of interest to you. In the references it says that dependent type theory is the interal language of locally cartesian closed categories. Also there is a paper called "Categorical Semantics for Higher Order Polymorphic Lambda Calculus" which discussed categorial semantics of the polymorphic lambda calculus (System F), but I do not know enough to understand it.  
> **username_2**: I'm not aware of an explicit formulation of such a cube, but Bart Jacobs [1] goes through various structures and axioms that can be required of fibrations that correspond to different type system. One might be able to assemble a cube from the chapter/sections and combinations thereof.  [1] B. Jacobs, Categorical Logic and Type Theory. Amsterdam: North Holland, 1999.  

---

## 0 answers

