?)

а сорцы этой чепухи имеются?

нашёл

где?

Есть кто, разбирающийся в cubical type theory?

Существует... Просто n-категории же.
И некоторые конструкции из них, могут быть и ∞
Определение —
https://ncatlab.org/nlab/show/(n%2Cr)-category

Таки ссылка на мануал —
Самое начало 166-й страницы Маклейна, смотреть за консрукцию T (T x) → T x, которая, очевидна, является T-алгеброй.

Более-менее неплохой обзор в книжке у тов. Ченг.
Ну и наверное, просто удобно рассматривать группоиды, потому чаще сейчас встретишь (∞,n)
Но это, надо сказать, что на практике, не совсем просто относительно n —
надо ещё для построений критерий фибрантности (в соответствующей модельной структуре).
https://en.wikipedia.org/wiki/Fibrant_object
https://ncatlab.org/nlab/show/fibrant+object
Например, в симплексах, это так называемые комплексы Кана (вполне так геометризируемое и несложное, в общем-то понятие) —
https://en.wikipedia.org/wiki/Kan_fibration
https://ncatlab.org/nlab/show/Kan+complex
Для различных кубических построений такие условия есть, вот например —
https://ncatlab.org/nlab/show/cubical+Kan+complex
Ну и где-то читал, что тов. Кан пытался начинать с кубических построений, но наткнувшись на технические сложности, перешёл на симплексы.
Для дисков Joyal'а тоже было, для опетопов где-то встречал, кажется...

Опетопы, это и есть n-операды, в общем-то :-)
Ну и вот fc-мультикатегории, это такие навороченные операды, правда, категория чОтко размерности 2.
А надо n. И будет обобщение опетопов и кубов ;-)

чо происходит?) нифига не понятно

"Кто здесь"? ;-)
Что именно непонятно?
Про монады, категории T-алгебр, Клейсли и возникающие сопряжённости понятно?

операды опетопы...

Ну это... Такое... ;-)

а тут только последнее местами пробелы

А для линейного лямбда исчисления такая же категориальная семантика как для линейной логики?

В качестве первого приближения, можно думать про операду, как про стрелку A⊗...⊗A → A в некой моноидальной категории.

моноидальной категории
такс