Декартово замкнутая категория

---

Декартово замкнутая категория — категория, допускающая каррирование, то есть содержащая для каждого класса морфизмов ${\displaystyle A\to B}$ некоторый объект ${\displaystyle A\Rightarrow B}$, представляющий его. Декартово замкнутые категории занимают в некотором смысле промежуточное положение между абстрактными категориями и множествами, так как позволяют корректно оперировать с функциями, но не позволяют, к примеру, оперировать с подобъектами.

С точки зрения программирования декартово замкнутые категории реализуют инкапсуляцию аргументов функций — каждый аргумент представляется объектом категории и используется как чёрный ящик. Вместе с тем выразительности декартово замкнутых категорий вполне достаточно, чтобы оперировать с функциями способом, принятым в λ-исчислении. Это делает их естественными категорными моделями типизированного λ-исчисления.

Категория C называется декартово замкнутой^[1], если она удовлетворяет трём условиям:

Категория, такая, что для любого её объекта категория объектов над ним декартово замкнута, называется локально декартово замкнутой.

В декартово замкнутой категории «функция двух переменных» (морфизм f:X×Y → Z) всегда может быть представлена как «функция одной переменной» (морфизм λf:X → Z^Y). В программировании эта операция известна как каррирование; это позволяет интерпретировать просто типизированное лямбда-исчисление в любой декартово замкнутой категории. Декартово замкнутые категории служат категорной моделью для типизированного ${\displaystyle \lambda }$-исчисления и комбинаторной логики.

Соответствие Карри — Ховарда предоставляет изоморфизм между интуиционистской логикой, просто типизированным лямбда-исчислением и декартово замкнутыми категориями. Определённые декартово замкнутые категории (топосы) предлагались как основные объекты альтернативных оснований математики вместо традиционной теории множеств.

---