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


  • 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
    Commented 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$ Commented Aug 5, 2020 at 5:41


Your Answer

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