笛卡尔闭范畴

把"函数空间"本身当作对象（高阶函数、柯里化）需要范畴具备指数对象 $B^A$。笛卡尔闭范畴（CCC）是有终对象、二元乘积与指数对象的范畴——它是 $\lambda$ 演算与函数式程序语言的语义模型，也是拓扑斯定义的基石。

需先掌握乘积与余积（终对象、二元积）、伴随函子与极限（$(-)\times A$ 的右伴随）与函子。

定义

范畴 $\mathcal{C}$ 称为笛卡尔闭，若

• 有终对象 $1$
• 对任意 $A,B$ 有二元积 $A\times B$
• 对任意 $B$，函子 $(-)\times B:\mathcal{C}\to\mathcal{C}$ 有右伴随 $(-)^B$：即存在对象 $B^A$（指数对象）与求值态射 $\mathrm{ev}:B^A\times A\to B$，使对每个 $f:C\times A\to B$ 存在唯一的 $\lambda f:C\to B^A$ 且 $\mathrm{ev}\circ(\lambda f\times\mathrm{id}_A)=f$

即 $\mathrm{Hom}(C\times A,B)\cong\mathrm{Hom}(C,B^A)$ 自然同构（柯里化）。

性质

• 例子：$\mathbf{Set}$（$B^A$ 是函数集）、$\mathbf{Cat}$、$\mathbf{Poset}$、预层范畴 $\mathbf{Set}^{\mathcal{C}^{\mathrm{op}}}$、拓扑斯都笛卡尔闭
• 反例：$\mathbf{Top}$、$\mathbf{Grp}$、$\mathbf{Vect}$（没有好的函数对象）不是 CCC
• 指数与积相容：$1^A\cong1$、$(B\times C)^A\cong B^A\times C^A$、$A^{B\times C}\cong(A^C)^B$
• Curry–Howard：CCC 的"类型=对象、程序=态射"对应 $\lambda$ 演算的简单类型；积对应合取、指数对应蕴含，是 Curry–Howard 同构的范畴论形态

例子

• $\lambda$ 演算模型：无类型 $\lambda$ 演算需要"自反对象"（$D\cong D^D$，如 Scott 域）；简单类型 $\lambda$ 演算在任意 CCC 中有模型
• 类型论语义：程序语言（Haskell、ML）的语义范畴通常是 CCC；curry/uncurry 就是伴随同构本身

应用

笛卡尔闭范畴是类型论与程序语义的基础（模型 $\lambda$ 演算、验证 Curry–Howard），也是拓扑斯定义的三条公理之一（与子对象分类器一起给出"集合的推广"）；它把乘积与余积的代数结构升级为"可计算"的结构。