Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

Simply typed lambda calculus is the internal language of Cartesian Closed Categories.

What category has its internal language the typed lambda calculus? And the untyped lambda calculus? Can we in fact consider it to be exactly the same as the simply typed calculus with the type constructor left implied?

share|cite|improve this question
up vote 5 down vote accepted

First of all, the internal language of a cartesian closed category is somewhat richer than simply-typed lambda calculus: it has finite product types in addition to function types. If you also want sum types then you have to pass to bicartesian closed categories, and if you want dependent versions of these then you basically have to work in an elementary topos. All this is discussed in [Lambek and Scott, Introduction to higher-order categorical logic]

The untyped lambda calculus is much more subtle. The absence of types make it particularly unsuited as an internal language for a category; but that is not to say category theory has no role to play in the study of its models.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.