Сумма и произведение | 235
Также нам хочется уметь как-то извлекать значения. По смыслу внутри суммы A+ B хранится либо объект
A либо объект B и мы не можем заранее знать какой из них, поскольку внутреннее содержание A + B от
нас скрыто, но мы знаем, что это только A или B. Это говорит о том, что если у нас есть две стрелки A → C
и B → C, то мы как-то можем построить A + B → C. У нас есть операция:
out( f, g) : A + B → C
f : A → C, g : B → C
При этом для того, чтобы стрелки inl, inr и out были согласованы необходимо, чтобы выполнялись
свойства:
inl ; out( f, g) = f
inr ; out( f, g) = g
Для любых функций f и g. Графически это свойство можно изобразить так:
A
inl
A + B
inr
B
out
f
g
C
Итак суммой двух объектов A и B называется объект A + B и две стрелки inl : A → A + B и inr : B →
A + B такие, что для любых двух стрелок f : A → C и g : B → C определена одна и только одна стрелка
h : A + B → C такая, что выполнены свойства:
inl ; h = f
inr ; h = g
В этом определении объект A + B вместе со стрелками inl и inr, определяет функцию, которая по
некоторому объекту C и двум стрелкам f и g строит стрелку h, которая ведёт из объекта A + B в объект
C. Этот процесс определения стрелки по объекту напоминает определение начального элемента. Построим
специальную категорию, в которой объект A+ B будет начальным. Тогда функция out будет катаморфизмом.
Функция out принимает две стрелки и возвращает третью. Посмотрим на типы:
f : A → C
inl : A → A + B
g : B → C
inr : B → A + B
Каждая из пар стрелок в столбцах указывают на один и тот же объект, а начинаются они из двух разных
объектов A и B. Определим категорию, в которой объектами являются пары стрелок ( a 1 , a 2), которые на-
чинаются из объектов A и B и заканчиваются в некотором общем объекте D. Эту категорию ещё называют
клином. Стрелками в этой категории будут такие стрелки f : ( d 1 , d 2) → ( e 1 , e 2), что стрелки в следующей
диаграмме коммутируют (не важно по какому пути идти из двух разных точек).
A
B
d
e
1
2
e 1
d 2
D