Глава 1. Категории как метасистемы

Где стоит глава

Том прошёл специальные области математики: анализ (III–IX), теорию множеств без выбора (X), алгебру и Галуа (XI), геометрию (XII), теорию чисел и дзету (XIII). Часть XIV — метатеоретический поворот: мы не добавляем «ещё одну тему», а разворачиваем язык, в котором все предыдущие части оказываются частными случаями. Этот язык — теория категорий.

В ToS-онтологии сдвиг получает свой характер. Категория — это E/R/R-структура высшего порядка: структура, чьи объекты суть сами системы, а стрелки — связи между ними. Поэтому сразу зафиксируем главную честную рамку, к которой вернёмся в финале части:

Категорный язык есть язык, а не предмет ToS. ToS не редуцируется к теории категорий; теория категорий служит метаязыком для описания связей ToS.

Эта глава делает первый шаг: даёт формальное понятие категории (возврат к Главе 1.5 об E/R/R), базовые универсальные конструкции (терминальный/инициальный объект, произведение, копроизведение), обзор стандартных категорий, и — принципиально для ToS — показывает их конструктивную природу (тип, а не «множество», без аксиомы выбора; мост к Части X). В конце мы строим первую конкретную категорию — категорию сетоидов SetoidCat, которая станет рабочей сценой Глав 14.2 и 14.6.

Категория как E/R/R-структура высшего порядка

Возврат к Главе 1.5. Система там — структура из элементов с ролями и правилами. Категория $\mathcal{C}$ есть та же триада, поднятая на уровень выше:

• Элементы: объекты (тип cat_obj) и стрелки/морфизмы (тип cat_mor $ab$);
• Роли: тождественная стрелка cat_id $a$ (нейтраль) и композиция cat_comp $fg$ (комбинатор);
• Правила: ассоциативность $f\circ (g\circ h)=(f\circ g)\circ h$ и единичные законы $\mathrm{id}\circ f=f$, $f\circ \mathrm{id}=f$.

В Rocq это полноценная запись.¹

$$‘RecordCategory‘:=\{‘ca{t}_{o}bj‘:\mathrm{Type};‘ca{t}_{m}or‘:‘ca{t}_{o}bj‘\to ‘ca{t}_{o}bj‘\to \mathrm{Type};\dots \}.$$

Тонкость, которая позже станет принципом. Поле cat_mor_eq задаёт своё равенство морфизмов — не лейбницево, а сетоидное (с явными рефлексивностью, симметрией, транзитивностью и совместимостью с композицией). Это не техническая деталь: уже здесь зашит P3 — различение «равно» и «изоморфно/эквивалентно», которое в Главе 14.3 станет центральным (P3_strictly_stronger_than_iso).

Итерация E/R/R. Применяя E/R/R к структурам, мы получаем новый уровень — категорию (структуру структур). Применяя E/R/R к категориям — получаем 2-категорию (категории категорий), и так далее. Часть XIV живёт на первой ступени этой лестницы; о её честной границе (нельзя собрать полную «категорию всех категорий» как один объект — малые/ограниченные категории функторов возможны, стена — именно «всех», на уровне вселенных) речь пойдёт в 14.7.

Универсальные конструкции: объект определяется ролью

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

• Терминальный объект $1$: в него из каждого объекта ведёт ровно одна стрелка ($\forall X,\exists !f:X\to 1$).
• Инициальный объект $0$: из него в каждый ведёт ровно одна стрелка.
• Произведение $A\times B$: объект с проекциями ${\pi }_A,{\pi }_B$, через который однозначно пропускается любая пара $f:C\to A$, $g:C\to B$.
• Копроизведение $A+B$: двойственно, с инъекциями.

{ Машинно проверено, что эти роли определены однозначно с точностью до изоморфизма: инициальный и терминальный объекты единственны (initial_unique_ up_to_iso, terminal_unique_ up_to_iso); изоморфизм есть отношение эквивалентности (iso_refl/iso_sym/iso_trans), всякий изоморфизм моничен и эпичен (iso_is_mono, iso_is_epi), композиция моно/эпи снова моно/эпи.²}

С точки зрения ToS универсальное свойство — это правило (L5), конституирующее объект через его роль. Не «что такое $A\times B$ внутри», а «как $A\times B$ ведёт себя по отношению ко всем остальным». Это ровно тот ход, который делает категорный язык метаязыком: он говорит о связях, не о субстанции.

Граница главы. Базовая запись Category.v даёт определения инициального и терминального объектов и свойства iso/моно/эпи (с единственностью с точностью до изоморфизма); сами произведения и копроизведения (как и экспоненты с классификатором подобъектов) здесь вводятся как стандартная категорная схема и будут машинно построены конкретно для SetoidCat в 14.6.

Стандартные категории

Одна запись Category охватывает всю обычную математику:

Категория	Объекты	Морфизмы
\Set	множества/типы	функции
$\mathbf{Grp}$	группы	гомоморфизмы
$\mathbf{Ring}$/$\mathbf{Field}$	кольца/поля	гомоморфизмы
${\mathbf{Vec}}_k$	векторные пространства	линейные отображения
$\mathbf{Top}$	топологические пространства	непрерывные отображения
$\mathbf{Man}$	гладкие многообразия	гладкие отображения
\Cat	категории	функторы (Глава 14.2)

В ToS-формализации каждая такая категория — конкретная запись типа Category. Базовый пример уже построен: TypeCat — категория типов и функций (равенство морфизмов — поточечное; TypeCat_valid, TypeCat_id_is_iso, TypeCat_comp_iso). Многообразия, группы, поля Частей XI–XII живут в своих категориях; Часть XIV даёт язык, объединяющий их.

Конструктивная природа: тип, а не «множество»

Классическая теория категорий часто говорит о «множестве объектов» — что в ToS-онтологии проблематично (Часть X: теория множеств без выбора; P4: нет завершённой бесконечности). ToS-категории работают на типах:

$$‘ca{t}_{o}bj‘:\mathrm{Type},‘ca{t}_{m}or‘ab:\mathrm{Type}.$$

В базовом категорном слое этой главы никакой аксиомы выбора не используется; равенство морфизмов — конструктивное сетоидное отношение (cat_mor_eq), не лейбницево. Category.v закрыт без аксиом (20 машинно проверенных лемм, 0 аксиом). Процессные категории дальше (14.6) имеют свою аксиомную цену (наследуют classic через Cauchy-слой) — это войдёт в карту границ 14.7.

Связь с Частью X прямая: там «множество» прочитано как режим (забывающий функтор от структуры), а не первичный объект. Категория наследует эту честность — её носитель есть тип (правило построения), а не завершённое множество-объект.

Первая новая рабочая категория части: SetoidCat

Чтобы метаязык не остался декларацией, в локально собранном слое src/category/ мы строим конкретную, не-тривиальную категорию — категорию сетоидов (первую новую рабочую категорию части после базовой TypeCat). Сетоид — это тип с заданным на нём отношением эквивалентности; морфизм сетоидов — функция, уважающая отношение; равенство морфизмов — поточечное (по отношению цели). Все законы категории выводятся покомпонентно из рефлексивности/симметрии/транзитивности отношения-цели.³

Почему именно SetoidCat? Потому что естественное равенство hom-множеств — сетоидное (равенство морфизмов cat_mor_eq), а не лейбницево. TypeCat использует поточечное лейбницево равенство значений ($f\sim g:=\forall x,fx=gx$); чтобы функториально принять hom-функтор $\mathrm{Hom}(x,-)$ произвольной категории, нужна область значений, где равенства самих hom-типов суть сетоидные отношения. Ею и служит SetoidCat: именно она в Главе 14.2 сделает возможной лемму Йонеды, а в Главе 14.6 окажется конструктивным предикатным топос-слоем (конечные пределы и копределы, декартова замкнутость, предикатный классификатор подобъектов).

Разбор E/R/R: категория как структура структур

Правила (L5). Конституция категории — ассоциативность и единичные законы (плюс совместимость композиции с равенством морфизмов). Универсальные свойства (терминал/инициал/ произведение) — правила-определения объектов через роль, не через устройство.

Роли (L4). «Тождество» — роль-нейтраль; «композиция» — роль-комбинатор; «терминал/инициал/произведение» — роли в сети стрелок; «изоморфизм/моно/эпи» — роли морфизмов (обратимость, лево-/право-сократимость).

Элементы (L1$+$P4). Конкретные типизированные данные: объекты cat_obj, морфизмы cat_mor $ab$ — типы, не множества; равенство морфизмов cat_mor_eq — сетоидное. Не элемент: «множество всех объектов» как завершённый Элемент.

Компонент	Что фиксирует	E/R/R-категория
ассоциативность + единичные законы; универсальные свойства	конституцию категории и её объектов	Правило (L5)
тождество$=$нейтраль; композиция$=$комбинатор; терминал/произв.$=$роли	статус стрелок и объектов	Роль (L4)
cat_obj, cat_mor $ab$ (типы), cat_mor_eq	типизированные носители	Элемент (L1$+$P4)

Что снимает разбор. Категория часто воспринимается как «ещё одна абстракция поверх множеств». ToS читает её как итерацию собственного устройства: E/R/R, применённое к структурам, даёт категорию — структуру структур. «Множество всех объектов» как завершённый Элемент при этом — категорная ошибка (носитель есть тип-правило, не завершённое множество-объект; P4, Часть X). А равенство морфизмов, взятое сетоидно, уже несёт зерно P3.

Что глава подготовила

Категория установлена как метасистема — E/R/R-структура высшего порядка — конструктивно (на типах, без аксиомы выбора в этом базовом слое), с понятиями инициального/терминального объекта и свойствами изоморфизма/моно/эпи, машинно проверенными в Category.v (20 Qed, 0 аксиом); произведения и копроизведения строятся конкретно для SetoidCat в 14.6. Построена первая новая рабочая категория части — SetoidCat, чьё сетоидное равенство морфизмов делает её правильной сценой для hom-функторов.

Дальше — Глава 14.2: функторы (структура-сохраняющие отображения категорий), естественные преобразования и — машинно, без аксиом — лемма Йонеды и полно-верное вложение Йонеды. Это даст точную форму тезису, зашитому уже в сетоидном равенстве этой главы: объект определяется своими ролями — категорная форма P3.

---

---

Часть: Часть XIV. Категория систем · Том: «Математика»

Навигация: ← Глава 7. Гипотеза Римана: три формы и карта границ — Часть XIII · Глава 2. Функторы, естественные преобразования, лемма Йонеды →

Footnotes

1. src/stdlib/Category.v (20 Qed, 0 аксиом; в origin/main): Record Category с полями cat_obj, cat_mor, cat_mor_eq (равенство морфизмов), cat_id, cat_comp и аксиомами cat_assoc, cat_id_l, cat_id_r, cat_comp_compat; плюс TypeCat, is_iso/is_mono/is_epi, is_initial/is_terminal, opposite_cat. ↩

2. Те же 20 Qed файла Category.v: iso_refl, iso_sym, iso_trans, iso_inv_unique, cat_id_unique, comp_mono, comp_epi, iso_is_mono, iso_is_epi, initial_unique_ up_to_iso, terminal_unique_ up_to_iso, iso_in_opposite и др. Все 0 аксиом. ↩

3. src/category/SetoidCategory.v (3 Qed, 0 аксиом): Setoid (носитель + st_eq/st_refl/st_sym/ st_trans), SetoidMor (отображение + sm_resp), SetoidCat как Category (SetoidCat_mor_eq_iff, SetoidCat_comp_map, SetoidCat_id_map); discrete_setoid как пример. Оговорка о воспроизводимости: слой src/category/ (13 файлов, 49 Qed, 0 аксиом, Print Assumptions$=$«Closed under the global context», commit 90ebd74) собран и проверен локально; синхронизация с основной веткой — пункт чек-листа (план v2). ↩