Оглавление
Объект натуральных чисел
-
Определение натуральных чисел в теории категорий
- NNO – объект с рекурсивной структурой, аналогичной натуральным числам.
- NNO задается глобальным элементом z и стрелкой s, удовлетворяющими определенным условиям.
- Треугольник и квадрат на диаграмме символизируют уникальность стрелок.
-
Эквивалентные определения и свойства
- В декартовых замкнутых категориях NNO определяется через уникальные значения стрелок.
- В категориях с конечным объектом и двоичными копроизведениями NNO – начальная алгебра эндофунктора.
- Каждый NNO является исходным объектом в категории диаграмм.
- Если декартова замкнутая категория имеет слабые NNO, то и ее фрагменты также имеют слабые NNO.
- NNO могут использоваться для нестандартных моделей теории типов.
-
Примеры NNO
- В Set стандартные натуральные числа – это NNO с z, выбирающим единственный элемент множества, и s – функцией-преемницей.
- В категории типов теории типов nat – это NNO.
-
Расшифровка NNO в топосах
- В топосах NNO может быть расшифровкой постоянного предварительного пучка.
- NNO в топосе E может быть представлено как сумма копий терминального объекта.
-
Ссылки и дополнительные материалы
- Ссылки на конспекты лекций и заметки о типах данных как алгебрах для эндофункторов.