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