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
---------
