![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
а теперь по существу
Mar. 2nd, 2019 10:32 amПять лет назад одно чучело спросило меня, как определить монаду в ZFC.
Мне тогда этот вопрос показался смешным. А на самом деле любопытно.
ZFC - это теория, и из нее можно построить категорию "множеств ZFC". Точнее, надо ее где-то строить. Сама по себе "категория категорий" - это тоже образец в теории категорий, а не модель теории категорий. Поэтому моделировать ZFC надо в каком-нибудь топосе. ZFC - это геометрическая теория, и можно построить универсальную модель, см., например, популярно у Оливии. Или, лучше, у нее же на слайдах.
Будет примерно то, что у населения ассоциируется с "теорией множеств", правда, логика снаружи этой теории.
Ну а теперь наоборот. Монада в ZFC.
Берем ZFC; определяем категорию (т.наз. малую категорию) - множество объектов, множество стрелок, функция "identity", бинарное отношение "композиция".
Определяем функтор из категории А в категорию В как пару функций А0 -> B0, A1 -> B1, удовлетворяющих нужным свойствам (сохраняет identity и композицию).
Определяем естественное преобразование α из функтора F в функтор G как семейство функций {αx: F[x] -> G[x] | x ∈А0}, так чтобы было совместимо со стрелками.
Мне тогда этот вопрос показался смешным. А на самом деле любопытно.
ZFC - это теория, и из нее можно построить категорию "множеств ZFC". Точнее, надо ее где-то строить. Сама по себе "категория категорий" - это тоже образец в теории категорий, а не модель теории категорий. Поэтому моделировать ZFC надо в каком-нибудь топосе. ZFC - это геометрическая теория, и можно построить универсальную модель, см., например, популярно у Оливии. Или, лучше, у нее же на слайдах.
Будет примерно то, что у населения ассоциируется с "теорией множеств", правда, логика снаружи этой теории.
Ну а теперь наоборот. Монада в ZFC.
Берем ZFC; определяем категорию (т.наз. малую категорию) - множество объектов, множество стрелок, функция "identity", бинарное отношение "композиция".
Определяем функтор из категории А в категорию В как пару функций А0 -> B0, A1 -> B1, удовлетворяющих нужным свойствам (сохраняет identity и композицию).
Определяем естественное преобразование α из функтора F в функтор G как семейство функций {αx: F[x] -> G[x] | x ∈А0}, так чтобы было совместимо со стрелками.
Затем определяем монаду как эндофунктор M: A -> A с двумя естественными преобразованиями, I0A -> M и M∘M -> M, чтобы соблюдались законы нейтральности и ассоциативности.
Вот и все, никаких моноидов.
Но это будет не теория монады, не "собственно монада", а модель монады в этой вашей ZFC (кстати, которой? Их бесконечное количество). Надо ж таки различать, где модель, а где теория.
Может быть, так и надо преподавать, для начинающих? Хз.
