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

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

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

С точки зрения

.

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

• в C имеется
  терминальный объект
  ;
• любые два объекта X, Y в C имеют произведение X × Y;
• любые два объекта Y, Z в C имеют экспоненциал Z^Y.

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

• декартовы произведения) и терминальные объекты — синглетоны
  .

• Категория Cat всех малых категорий (и функторов в качестве морфизмов) декартово замкнута; экспоненциал C^D — это категория функторов из D в C с естественными преобразованиями в качестве морфизмов. Также существует категория произведения и терминальный объект — категория 1 из одного объекта и одного морфизма.

• Элементарный топос является декартово замкнутой категорией по определению.

• Алгебра Гейтинга (англ. Heyting algebra) также является стандартным примером декартово замкнутой категории. Так как булева алгебра является её частным случаем, она тоже всегда декартово замкнута.

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

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

• Curien P.-L. Categorical combinatory logic.-- LNCS, 194, 1985, pp.~139—151.
• Roy L. Crole, Categories for Types, Cambridge University Press, 1994.

Для улучшения этой статьи желательно: Проставить сноски, внести более точные указания на источники. Оформить список литературы. После исправления проблемы исключите её из списка. Удалите шаблон, если устранены все недостатки.