deep-econom (deep_econom) wrote,
deep-econom
deep_econom

общая теория всего как теория суперкатегорий

akuklev пришел к моим же построениям )
сравните

------------
общая теория структур или к вопросу о протологике
https://deep-econom.livejournal.com/77369.html

теория описания всего
https://deep-econom.livejournal.com/94281.html

-----------
Обобщённые мультикатегории

Ходячей моделью финитарной алгебраической теории, как известно, является мультикатегория. Объекты мультикатегории — типы теории, а морфизмы — выражения (т.е. композиции) операций теории. Ходячая модель ещё называется “непредвзятым представлением”, потому что тут не выделяются “базовые операции и композиции” и “непредвзятое представление” остаётся одним и тем же независимо от того, какие операции взять за базовые, если результат один и тот же.

Напомню, что мультикатегория — это как категория, только стрелочки у нас не Ob -> Ob, а List[Ob] -> Ob.

Я думал-думал и понял, что если в “алгебраическую” теорию добавить типы типов и полиморфизм (полиморфизм оказывается стратифицированным частным случаем зависимостей внутри контекста), то ходячей моделью будет обобщённая мультикатегория со стрелками вида Ctx[Ob] -> Ob, где Ctx — обобщённая мультикатегория, представляющая алгебру типов данной алгебры, а обозначение Ctx[Ob] обозначает порождения свободной Ctx-алгебры над Ob. В случаи зависимых теорий типов без стратификации выходит некий гордиев узел — обобщённая мультикатегория, обобщённая над самой собой. Но эта штуковина оказывается корректной, если сигнатуры всех операций можно представить в форме bi-directional type checking/inference.

В общем, в первый раз я доконца понял, в каком-таком виде надо представить теорию категорий как обобщённую алгебраическую теорию, чтобы естественной доктриной моделей являлась категория виртуальных двойных категорий — вариант одновременно включающий и понятие внутренних категорий, и понятие обогащённых категорий.
https://akuklev.livejournal.com/1281079.html
---------
Tags: понимание
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic
  • 0 comments