Глава 6. Процессы как универсальные конструкции; Setoid как топос

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

Главы 14.1–14.3 работали внутри уровня, 14.4 связала уровни сопряжением (P2), 14.5 подняла сопряжение до языка двойственностей. Эта глава о P4 (Конечная актуальность) — о том, как ToS понимает универсальные конструкции: пределы, копределы, экспоненты, классификатор подобъектов. У ToS здесь два прочтения, и оба отказываются от «завершённого бесконечного объекта»:

• Процессное (P4 буквально): предел и копредел суть процессы. Произведение — процесс пар, уравнитель — процесс разностей, копредел — сам процесс.
• Сетоидно-топосное (абстрактное): категория сетоидов $\text{SetoidCat}$ несёт топосный набор структур — конечные (ко)пределы, декартову замкнутость, предикатный классификатор подобъектов, — и все они конструктивны.

Ярусы (честно, проверено по зависимостям). Процессное прочтение — процессный слой, консервативно относимый к ярусу classic (зависит от ProcessArithmetic, который импортирует Classical; точный статус конкретных лемм — по Print Assumptions); в origin/main. Сетоидно-топосное прочтение — 0 аксиом по локальному build, но локальный слой src/category/ (коммит 90ebd74, ожидает push). Контраст поучителен: конкретное P4-прочтение тащит L3 (аналитика над ℚ), а абстрактное топосное — полностью конструктивно.

Процессное прочтение: пределы суть процессы

Под P4 универсальная конструкция не «собирается» из завершённого конуса, а вычисляется поэтапно — т. е. есть процесс. ¹

Произведение — процесс пар. $A\times B$ есть поточечное спаривание process_product: $n\mapsto (R_{1}n,R_{2}n)$; проекции возвращают компоненты (product_fst/_snd), спаривание единственно (product_universal), и если обе компоненты Коши, то и произведение (product_cauchy).

Уравнитель — процесс разностей. $\mathrm{eq}(f,g)$ есть equalizer_process $fg=\lambda n.fn-gn$. Он сходится к нулю ровно тогда, когда $f$ и $g$ эквивалентны как процессы (equalizer_converges и обратно equalizer_ zero_ means_ equiv). То есть «совпадать» для процессов — это уравнитель стремится к нулю, а не «равны как завершённые объекты».

Копроизведение — переплетение. $A+B$ есть чередование (process_coproduct): чётные позиции несут $R_1$, нечётные — $R_2$; инъекции попадают точно в свои места ($R_1(k)$ в позицию $2k$, $R_2(k)$ в $2k+1$ — coproduct_inj1/_inj2).

Флагман P4: копредел есть процесс

Высшая точка процессного прочтения — направленный копредел. Цепь процессов $a_0,a_1,a_2,\dots$ не нуждается в «завершённом» копределе-объекте: им служит диагональ — сам процесс

$$‘directe{d}_{c}olimit‘\mathrm{chain}=\lambda n.\mathrm{chain}nn$$

(colimit_diagonal). Это и есть P4 во плоти: «копредел цепи $a_0,a_1,\dots$ есть сам процесс $a$» — никакого завершённого предельного объекта не требуется и не вводится.

Тот же урок проходит через весь том: $R$ — процесс (Часть IV), $\overline{Q}$ — башня без максимальной ступени (Часть XI), многообразие — процесс (Часть XII). Категорно он называется одним словом: копредел — сам процесс, а не завершённый объект сверх него. Потенциальная бесконечность (процесс) заменяет актуальную (завершённый копредел) — ровно это P4 и требует.

Процессная категория

Когда процессы упаковываются в категорию (объекты — процессы, морфизмы — согласованные отображения), включается L3: формализация процессной категории импортирует Classical. ² Это честная граница яруса: элементарные процессные определения просты, но уже уравнитель-Коши (equalizer_cauchy) и подобные опираются на аналитику ℚ-Коши, а та импортирует Classical. Поэтому процессную сторону мы консервативно относим к ярусу classic, а не «0 аксиом» — точный статус конкретных лемм сверяется через Print Assumptions (карта границ — 14.7).

Сетоидно-топосное прочтение: $\text{SetoidCat}$ как топосный набор

Абстрактная сторона предъявляет универсальные конструкции в категории сетоидов $\text{SetoidCat}$ (объекты — типы с эквивалентностью, морфизмы — уважающие её отображения; см. 14.1). Здесь собран топосный набор структур — и весь он 0-аксиомен.

Конечные пределы. Терминальный объект — единичный сетоид (setoid_terminal); бинарные произведения с универсальным свойством (setoid_prod_beta1/_beta2, setoid_ prod_ unique); уравнители (eq_equalizes, eq_univ, eq_unique). Математически терминал$+$бинарные произведения$+$уравнители образуют стандартный базис всех конечных пределов; машинно проверены эти базовые компоненты и их универсальные свойства. ³

Конечные копределы. Инициальный объект — пустой сетоид (setoid_initial); копроизведения с универсальным свойством (coprod_beta1/_beta2, coprod_ unique). Инициал$+$бинарные копроизведения образуют стандартный базис конечных копределов (машинно — эти компоненты и их универсальные свойства). ⁴

Декартова замкнутость. Экспонента $B^A$ — сетоид отображений $A\to B$ с поточечным равенством, с применением (setoid_eval) и каррированием (setoid_curry); универсальное свойство — биекция

$$\text{Hom}(C\times A,B)\cong \text{Hom}(C,B^A)$$

(exp_beta, exp_unique). Значит $\text{SetoidCat}$ декартово замкнута. ⁵

Классификатор подобъектов. Объект истинностных значений $\Omega =(Prop,\leftrightarrow )$ (на уровне текущего сетоидного слоя) с истиной true и характеристической стрелкой char: уважающий предикат соответствует стрелке $A\to \Omega$, а подобъект $\{a\mid Pa\}$ — праобраз истины (subobject_commute, subobject_univ, subobject_unique). ⁶

Итог. $\text{SetoidCat}$ несёт конечные (ко)пределы$+$декартову замкнутость$+$предикатный классификатор — конструктивный предикатный (элементарный) топос-слой, целиком 0-аксиомный (по локальному build; после push — финальная сверка Print Assumptions). Это конкретная «структура структур», обещанная в 14.1.

Честная граница: предикатный, не полный топос

Классификатор классифицирует уважающие предикаты (конструктивные подсетоиды), а не произвольные мономорфизмы: для последних нужна факторизация образа, которой мы не строим. Поэтому честно говорить о предикатном топос-слое, а не о полном элементарном топосе. Это не дефект конструкции, а её точная область: предикатный классификатор — ровно то, что даёт конструктивная сетоидная установка.

P4 в обоих прочтениях. Топосные конструкции — P4 в той же мере, что и процессные. Произведение финитно актуально (пара — конечный носитель); экспонента $B^A$ — роль-уровневый внутренний hom (сетоид с поточечным равенством), не мощностная операция над завершёнными множествами (ср. Часть X); $\Omega =(Prop,\leftrightarrow )$ (на уровне сетоидного слоя) — объект значений с логической эквивалентностью, не «множество всех подмножеств». Универсальное свойство всюду — правило единственной факторизации, а не завершённый объект над всеми конусами. Оба прочтения суть одно P4-движение: потенциальное вместо актуального.

Разбор E/R/R: универсальные конструкции как E/R/R

Правила (L5). Универсальные свойства ($\beta$, $\eta$-единственность) конституируют каждую конструкцию; на процессной стороне — сохранение Коши; на топосной — поточечное/покомпонентное сетоидное равенство (роль-уровень, не лейбницево).

Роли (L4). Проекции/инъекции/медиаторы (пределы/копределы); применение/каррирование (экспонента); char/классификатор (подобъекты); процесс-как-копредел — роль самой P4.

{

Элементы (L1$+$P4). Конкретные данные: пары $(R_{1}n,R_{2}n)$, разности $fn-gn$, переплетение, диагональ $\mathrm{chain}nn$; сетоидные носители, $Prop$. Не элемент: завершённый бесконечный предел/копредел (процессная сторона его не вводит); и кардинал $B^A$ / классификатор произвольных моно (топосная сторона даёт лишь предикатный).}

Компонент	Что фиксирует	E/R/R-категория
универсальные свойства ($\beta$/$\eta$); Коши-сохранение; сетоидное равенство	конституцию конструкций	Правило (L5)
проекции/медиаторы; eval/curry; char; процесс-как-копредел	статус универсальных стрелок	Роль (L4)
пары, разности, диагональ; сетоиды, $Prop$	финитно актуальные носители	Элемент (L1$+$P4)

Диагностика P4. Обе стороны суть одно: нет завершённой бесконечности. Копредел — процесс, а не объект; экспонента — роль-уровневый hom, а не кардинал; классификатор — над уважающими предикатами, а не над всеми моно. P4 здесь конструктивно строит, а не запрещает.

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

Универсальные конструкции получили два согласных прочтения. Процессное (P4 буквально): произведение — процесс пар, уравнитель — процесс разностей, копроизведение — переплетение, а копредел есть сам процесс (диагональ $\mathrm{chain}nn$) — флагман P4. Сетоидно-топосное: $\text{SetoidCat}$ несёт конечные (ко)пределы, декартову замкнутость и предикатный классификатор подобъектов — конструктивный предикатный топос-слой. Оба прочтения суть одно P4-движение: потенциальное вместо завершённого.

{

Ярусы (честно). Процессная сторона — ProcessLimitColimit.v + ProcessCategory.v — процессный слой, консервативно отнесённый к classic (аналитика ℚ-Коши; ProcessCategory.v прямо импортирует Classical); в origin/main. Топосная сторона — пять файлов src/category/ (SetoidProducts 4, SetoidEqualizers 3, SetoidCoproducts 4, SetoidExponential 2, SetoidClassifier 4 = 17 Qed) — 0 аксиом по локальному build, но локальный слой (90ebd74, ожидает push). Честная граница: предикатный, не полный топос (нужна факторизация образа).}

Дальше — Глава 14.7, финал: вся ToS как категория (E/R/R сам есть категория); мост к теории типов (Карри–Ховард); и карта границ Части XIV — стены вселенных («категория всех категорий/предпучков велика»), ярус classic, континуальная цена, — собранные в одном месте.

---

---

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

Навигация: ← Глава 5. Сопряжения как универсальный язык двойственностей · Глава 7. Синтез: вся ToS как категория; мост к теории типов; карта границ →

Footnotes

1. src/process/ProcessLimitColimit.v (0 Admitted; в origin/main). Шапка файла указывает AXIOMS: none; но модуль зависит от процессного стека, где ProcessArithmetic импортирует Classical, поэтому процессную сторону мы консервативно относим к ярусу classic (точный статус — по Print Assumptions). Ключевые имена: process_product, product_universal, equalizer_process, equalizer_converges, equalizer_ zero_ means_ equiv, process_coproduct, coproduct_inj1/_inj2, directed_colimit и др. ↩

2. src/process/ProcessCategory.v (20 Qed, 0 Admitted; наследует classic — «inherited from ProcessNoetherian», импортирует Classical; в origin/main). Рядом — src/process/ProcessUniversalAdjunction.v (24 Qed; процессный слой; в origin/main): универсальное сопряжение на процессной стороне. ↩

3. src/category/SetoidProducts.v (4 Qed) и SetoidEqualizers.v (3 Qed); 0 Admitted, 0 аксиом; локальный слой src/category/ (90ebd74, ожидает push): unit_setoid/setoid_terminal, prod_setoid/setoid_fst/_snd/_pair, setoid_prod_beta1/_beta2/_unique; eq_setoid/eq_incl/eq_mediator, eq_equalizes/eq_univ/eq_unique. ↩

4. src/category/SetoidCoproducts.v (4 Qed, 0 Admitted, 0 аксиом; локальный слой): empty_setoid/setoid_initial, sum_setoid/inl_mor/inr_mor/sum_copair, coprod_beta1/_beta2/_unique. ↩

5. src/category/SetoidExponential.v (2 Qed, 0 Admitted, 0 аксиом; локальный слой): exp_setoid, setoid_eval, curry_app, setoid_curry, exp_beta, exp_unique. ↩

6. src/category/SetoidClassifier.v (4 Qed, 0 Admitted, 0 аксиом; локальный слой): omega_setoid $=(Prop,\leftrightarrow )$, setoid_true, char, char_self, sub_setoid, subobject_commute/_univ/_unique. ↩