---
title: "Cartesian Closed Categories and Typed λ-Calculi"
authors:
  - "Joachim Lambek"
year: 1986
venue: "Combinators and Functional Programming Languages, LNCS 242"
arxiv: null
doi: "10.1007/3-540-17184-3_44"
source: "https://doi.org/10.1007/3-540-17184-3_44"
topics:
  - category-theory
  - lambda-calculus
  - cartesian-closed
seed_rank: 151
seed_batch: "prefill-2026-08-13"
reviewed: "2026-08-13"
pool: "maths-foundations"
relevance_score: 9
cites:
  - title: "Introduction to Higher Order Categorical Logic"
    url: "https://doi.org/10.1017/CBO9780511620263"
    year: 1986
    arxiv: null
    doi: "10.1017/CBO9780511620263"
  - title: "Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes"
    url: "https://doi.org/10.1111/j.1746-8361.1958.tb01464.x"
    year: 1958
    arxiv: null
    doi: "10.1111/j.1746-8361.1958.tb01464.x"
  - title: "Aspects of higher order categorical logic"
    url: "https://doi.org/10.1090/conm/030/749773"
    year: 1984
    arxiv: null
    doi: "10.1090/conm/030/749773"
  - title: "Pre-recursive categories"
    url: "https://doi.org/10.1016/0022-4049(82)90060-3"
    year: 1982
    arxiv: null
    doi: "10.1016/0022-4049(82)90060-3"
  - title: "Closed Categories"
    url: "https://doi.org/10.1007/978-3-642-99902-4_22"
    year: 1966
    arxiv: null
    doi: "10.1007/978-3-642-99902-4_22"
  - title: "Functional completeness of cartesian categories"
    url: "https://doi.org/10.1016/0003-4843(74)90003-5"
    year: 1974
    arxiv: null
    doi: "10.1016/0003-4843(74)90003-5"
  - title: "Functionals defined by recursion."
    url: "https://doi.org/10.1305/ndjfl/1093956080"
    year: 1967
    arxiv: null
    doi: "10.1305/ndjfl/1093956080"
  - title: "Proceedings of the Conference on Categorical Algebra, La Jolla, 1965"
    url: "https://doi.org/10.1007/978-3-642-99902-4"
    year: 1966
    arxiv: null
    doi: "10.1007/978-3-642-99902-4"
  - title: "Algèbres graphiques (sur un concept de dimension dans les langages formels)"
    url: "https://www.numdam.org/item/CTGDC_1981__22_3_249_0/"
    year: 1981
    arxiv: null
    doi: null
see:
  - "041-introduction-to-higher-order-categorical-logic"
---

# Cartesian Closed Categories and Typed λ-Calculi

## One-sentence takeaway

Lambek shows that the simply typed λ-calculus with products is the internal language of a cartesian closed category: types are objects, typed terms are morphisms, and βη-equations are the CCC laws.

## Why it matters here

This is the compact Curry–Howard–Lambek bridge Anoptic language work needs before the full Lambek–Scott book: query combinators, command arrows, and typed λ fragments should be designed as morphisms in a CCC, not as ad-hoc AST rewrites.

## Key ideas

- A type \(A\) is an object; a term \(x:A \vdash t:B\) is a morphism \(A \to B\), and a multi-variable term is a morphism out of a product.
- Product types, pairing, and projections interpret the cartesian structure; function types, λ-abstraction, and application interpret exponentials via currying and evaluation.
- β- and η-equality of typed terms correspond to the universal properties of products and exponentials, so program equations are diagram equations.
- The same correspondence reads as intuitionistic propositional logic: products are conjunction and exponentials are implication.
- The free CCC generated by a typed λ-theory is the canonical syntactic model; any CCC is a semantic model of the calculus.

## Caveats

## Links

- DOI: [10.1007/3-540-17184-3_44](https://doi.org/10.1007/3-540-17184-3_44)
- Chapter: https://link.springer.com/chapter/10.1007/3-540-17184-3_44