7
$\begingroup$

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

Improve this question
$\endgroup$
2
  • 2
    $\begingroup$ I think 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. $\endgroup$
    – Labbekak
    Aug 2, 2020 at 12:17
  • 2
    $\begingroup$ 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. $\endgroup$
    – Henning Basold
    Aug 5, 2020 at 5:41

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.