Category: наука

Category was added automatically. Read all entries about "наука".

ДР Цертуса 2011

(no subject)

Настоящим объявляю, что все мои персональные данные, тексты, фотографии, рисунки, переписка и т.п. являются объектами моего авторского права (согласно Бернской Конвенции), и оповещаю «ЖЖ» (LiveJournal, Inc / SUP Media) о том, что разглашение, копирование, распространение моей личной информации в коммерческих целях равно как и любые другие противоправные действия по отношению к моему профилю в социальной сети строго запрещены.

Для коммерческого использования всех вышеупомянутых объектов авторского права в каждом конкретном случае необходимо мое письменное разрешение.

Гёттинген
17 января 2015 г.
Александр Куклев
ДР Цертуса 2011

Равенство Лейбница как кодирование Чёрча и Cedille

А вот все говорят, что равенство Лейбница это импредикативное кодирование равенство Мартин-Лёфа.

А вот Cedille получается кодировать индуктивные типы через зависимые пересечения соответствующего им типа импредикативного кодирования, и принципа индукции. Разберём на примере натуральных чисел.

Вот тип алгебр над сигнатурой натуральных чисел:
```
NatAlg := ∀[T : ∗], (succ : T -> T, zero : T)
```

Сами натуральные числа Nat — алгебра, свободно порождённая succ и nat, её можно также охарактеризовать как инициальную среди всех таких алгебр, т.е. из неё существует уникальный гомоморфизм в любую такую алгебру: т.е. в частности это означает, что берём элемент `n : Nat`, берём алгебру `A : NatAlg`, замешиваем их и получаем некий элемент A.T. Можно попробовать сказать, что элементы `Nat` это и есть такие “черные ящики”, превращающие всякую Nat-алгебру в её элемент:
```
Nat-ish := ∀[T : ∗], (T -> T) -> T -> T
```

Это и есть нумералы Чёрча, несложно показать что этот тип имеют выражения следующего вида:
```
zero := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ n
one := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ f(n)
two := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ f(f(n))
three := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ f(f(f(n)))
...
```

А следующая функция превращает нумерал в следующий нумерал:
```
succ(m : Nat-ish) := ∀(T : ∗), (\f : T -> T) ↦ (\n : T) ↦ (m(f))(f(n))
```

Все синтаксически-выразимые объекты типа Nat-ish суть натуральные числа. Но, ежели у подлежащей теории есть теоретикомножественные модели, то в этих моделях тип Nat-ish неизбежно будут населять ещё и бестии, невыразимые синтаксически. Однако можно ведь попытаться выделить среди них “настоящие”, т.е. те, для которых работает математическая индукция. Давайте запишем тип, выражающий математическую индукцию, т.е. позволяющий доказать предикат P(n : Nat) для всех n, обладая доказательствами базы индукции P(0) и шага индукции P(n) -> P(succ(n)):

Nat-ly := (n : Nat-ish) ↦ ∀[P : Nat-ish -> ∗], (step : ∀[n : Nat-ish], P(n) -> P(succ n)) -> (base : P(zero)) -> P(n)

В Cedille есть способ выделить среди типа Nat-ish элементы, которые сами себе доказательство индукции (термы n, которые могут быть типизированны одновременно как элементы Nat-ish и как элементы Nat-ly(n) для самого себя):
```
Nat := (n : Nat-ish, n : Nat-ly(n))
```

Вот для этого типа в Cedille можно показать, что это в самом деле тип натуральных чисел.

* * *

Теперь давайте попробуем проделать то же самое для типа равенства. Равенство-лейбница термов `x y : T` записывается как тип
```
Id-ish[T : ∗](x y : T) := ∀[P : T -> ∗], P(x) -> P(y)
```

Запишем также терм
```
refl[T : ∗](x : T) : ∀(P : T -> ∗), (\p : P(x)) ↦ p
```
и обратим внимание, что `refl[T](x) : Id-ish[T](x, x)`.

Теперь давайте вспомним как устроена индукция для равенства Мартин-Лёфа:
```
Id-ly[T : ∗](x y : T) := (p : Id-ish[T](x, y)) ↦ (∀[P : Id[T] -> ∗], P(refl)) -> P(p)
```

Кто-нибудь уже изучал тип `Id-ish[T : ∗](x y : T) := (p : Id-ish[T](x, y), p : Id-ly[T](x, y)(p))` в Cedille?
ДР Цертуса 2011

Пожалуйтесь на бога в вышестоящую инстанцию

(из частной переписки)

Сама идея, что физическая реальность не является вопросом компромисса, как-то не укладывается в головах.

Политики, журналисты, колумнисты, общественные деятели привыкли, что всякий, кто что-либо заявил публично по какому-то вопросу, в дальнейшем интересуется не содержательной стороной вопроса, а отстаиванием своей правоты.
Диалог с добросовестным учёным вызывает у них чудовищное недоумение. Учёный то меняет мнение “как флюгер”, как только выяснятся новые обстоятельства, то оказывается упрямым как террорист, и не идёт ни на какие на переговоры — нет чтобы как современные гибкие люди, сдать немножечко своей позиции, ну хотя бы чтобы показать цивилизованность и договороспособность, согласиться хотя бы для приличия, что 2 + 2 не 4, а хотя бы ну может быть 3,8 или 4,1. От большого уважения к бесноватому гению они готовы предложить аж 3,95, но “варвары” от науки просто с цепи сорвались со своим невероятно раздутым эго, продолжают настаивать на том, что 2 + 2 = 4.
То ли дело вирусолог Х, — сетует условный колумнист Фокуса, — вот тот, как только раскритиковали его пресс-релиз, что 2 + 3 = 6, сразу пошёл на встречу и согласился на пять с половиной. Вот цивилизованный человек!

Но ладно бы только это, ведь они же массово пытаются торговаться со стихией, как будто можно ставить ей условия или хитрить с ней путём подгонки фактов. “Мы готовы закрыть школы, но только по средам и пятницам.” Ну молодцы что готовы. Природе/богу похер что вы готовы, а что нет. Обидно, что бессердечная стихия не оценила и без того титанические старания? You feel offended? Ну не знаю, пожалуйтесь на бога в вышестоящую инстанцию, или назло маме отморозьте уши. Только нас в это не втягивайте.
ДР Цертуса 2011

Hemifields (освежая в памяти...)

Напомню, что для поле (тело) можно эквивалентно определить как (коммутативное) кольцо, где
1) Для всякого x ≠ 0 существует x⁻¹ такое, что x⁻¹x = xx⁻¹ = 1;
2) Для всякого x ≠ 1 существует x*, такое что x* = 1 + xx* = 1 + x*x.

Дело в том, что можно определить x* через (1 - x)⁻¹, а x⁻¹ через x = 1 - x*⁻¹. Для полуколец в зависимости от того, что выбрать, получатся неэквивалентные результаты, т.к. там нет операции «-».

Если выбрать вариант (1), получатся широко известные полуполя, такие как полуполе неотрицательных рациональных чисел или тропическое полуполе. Они превосходно поддаются классификации: на самом деле, все полуполя либо являются полями, либо являются обобщениями указанных двух примеров — тропическими алгебрами частично-упорядоченных групп, либо неотрицательными частями частично-упорядоченных полей и их факторполуполями, см. https://arxiv.org/pdf/1709.06923.pdf.

Если выбрать вариант (2), получаются штуковина, устоявшегося названия которой я не нашёл, назовём пока гемиполями (hemifield) и гемителами. Сюда, разумеется, входят все поля/тела. Но кроме того гемителами являются по определению все полукольца со звездой (star semirings, см. http://stedolan.net/research/semirings.pdf), например полукольцо регулярных выражений, где сложение это |, умножение конкатенация, единица пустая строка, а звёздочка “нуль или более раз”. Канонические примеры гемиполей — гемиполя индуктивных типов данных с точностью до изоморфизма. Сложение это Either[X, Y], умножение Pair[X, Y], звёздочка — List[T]. Для индуктивных типов данных верно, что вообще всякое невырожденное уравнение X = Polynome[X] имеет решение. Это утверждение для обычных полей означало бы алгебраическую замкнутость.

Мне много-много лет интересна задача классификации алгебраически-замкнутых (в указанном выше смысле) гемиполей.

* * *

Напомню, что локальными кольцами называются кольца, у которых для всякого x существует по меньшей мере либо x*, либо x⁻¹. Попробуем назвать локальными полукольцами такие полукольца, у которых для всякого x существует по меньшей мере либо x*, либо x⁻¹. Это общее обобщение полутел и гемител. Имеют ли какие-то хорошие свойства локальные полукольца, являются ли они в каком-то смысле естественными? Имеют ли они какое-то отношение к локализациям, как в случае колец? Существует ли для них какой-то вариант теоремы о том, что все проективные модули (бисемимодули?) над ними обладают базисом?
ДР Цертуса 2011

“пересказал Бродского своими словами”

Кто живёт в разноязычных средах, тому наверняка знакома проблема, когда хочешь поделиться стихами, песней, да хотя бы шуткой на каком-то языке, которым собеседник не владеет, а в переводе уже не то. Да и не только в языке дело, культурный контекст нужен.

Вот если хочешь поделиться восторгами по поводу музыки, видом с горной вершины, невероятного здания, картины, скульптуры — можно показать близким и друзьям, и хоть в какой-то степени, но всё-таки оценят! А не оценят, так хоть заинтересуются...

Но есть такая очень важная для меня сторона жизни, где я своими восторгами я обычно не могу поделиться ни с кем из близких. Там происходят революции, там прямо при нас, прямо сегодня открывают новые континенты, а показать не могу, не могу поделиться.

Симон Анри в прошлом году придумал слабые модельные категории — это настолько круто, что учебники (конечно, не школьные) переписывать можно, он вообще на верном пути в ближайшее время доказать гипотезу Симпсона и вскультивировать целиком ландшафт этой науки. Эмили Риль — придумала принципиально новый подход к проблеме когерентности, красиво как симфония. Две недели назад Пит показал мне с коллегами Эвдоксовы вещественные числа — способ определить вещественные числа через квазиэндоморфизмы на абелевой группе целых. Харальд Хельфготт (тот самый мужик, который недавно слабую гипотезу Гольдбаха доказал, профессорствующий, кстати, у нас в Гёттингене) — оптимизировал решето Эратосфена просто невероятно круто. Это просто четыре рандомных вещи, но оно там такое всё, искрится как фейерверк и всё время что-то новое. Это так красиво, что дух захватывает, это окрыляет, этим хочется делиться, это хочется показывать. Но тот язык, на котором написана эта поэзия, к сожалению, не знает почти никто, и культурный контекст за вечер не перескажешь.

Вот есть, скажем, Алиса, ей почти восемнадцать, она очень талантливая, в том числе и в точных науках — по меркам нефизматшкольника ну просто очень много знает, и иногда ей бывало даже интересно понять, чем это я таким занимаюсь. Но я даже не представляю, с какого конца мне зайти, чтобы хоть как-то, хоть совсем на пальцах начать рассказывать про то, чем мы занимаемся и почему это так круто.

Спасибо воть только SpaceX с их космическими кораблями — их старты и посадки я ни раз смотрел и с Алисой и с Настей, а как Айлин подрастёт, и с ней буду смотреть старты в прямом эфире и прикольные видео про устройство ракетных двигателей и вообще космической техники.
ДР Цертуса 2011

Интуиционистская лемма Цорна

Как известно, в интуиционистских теориях типов определимы только вычислимые тотальные `f : A -> B`. Теория типов не утверждает, что внутри типа функций `A -> B` не живёт ещё каких-нибудь (невычислимых) функций, но вот конкретно предьявить можно только тотально-вычислимые. А это означает, что у нас не может быть Тьюринг-полноты, т.е. как бы не была совершенна наша конкретная интуиционистская теория типов, найдутся такие (Тьюринг-)вычислимые функции из `A` в `B`, которые мы не сможем выразить термом `f : A -> B`. Тем не менее, в некоторых интуиционистских теориях типов, поддерживающих индуктивно-индуктивные фактортипы (гомотопическая теория типов и её близкие родственники) можно определить монаду ℧ частично-вычислимых функций, т.е. функций, которые могут в процессе вычисления значения “зависнуть”. И тут уж верно, что термом `f : A -> ℧(B)` можно выразить любую вычислимую функцию из `A` в `B`. Но этот тип, разумеется, содержит кроме тотально-вычислимых функций ещё и функции, которые на каких-то аргументах могут зависать.[1]

Разумеется, мы можем записать вот такой тип:
Property Totality[on f : X -> ℧(Y)]:
  ∀x : X, f(x) ≠ ⊥
Разумеется было бы прикольно иметь оператор
totalize(f : X -> ℧(Y) with Totality) : X -> Y
Правильно ли я понимаю, существование такого оператора это в точности интуиционистская Лемма Цорна?

(NB: Без закона исключённого третьего, из Леммы Цорна никак не доказываются Аксиома Выбора и её эквиваленты.[2])

(NB: Разумеется, наличие такого оператора “небесплатно”. Как минимум, его наличие превращает разрешимость проверки доказательств в полуразрешимость. Но вполне возможно, что оно ещё как-нибудь хитро ломает вычислимость.)

[1] https://arxiv.org/abs/1610.09254
[2] John L. Bell, “Some New Intuitionistic Equivalents of Zorn’s
Lemma”, http://publish.uwo.ca/~jbell/Some%20New%20Intuitionistic%20Equivalents%20of%20Zorn.pdf
ДР Цертуса 2011

Карри-Говард для FOL

Как все тут знают, по соответствию Карри-Говарда интуиционистской логике высказываний (логике нулевого порядка) соотведствует просто-типизированное лямбда-исчисление с произведениями STLC.

Утверждениям в логике соответствуют типы в STLC, доказательствам утверждений — термы соответствующих типов. У STLC с произведениями есть прекрасная категорная семантика — декартово-замкнутые категории.

С логикой первого порядка всё чуть сложнее. Там кроме утверждений появляются предикаты и отношения — утверждения, зависимые от одной или нескольких переменных, которые тоже имеют свои типы, в зависимости от подлежащей теории. Например, если мы в рамках логики первого порядка описываем линейные пространства, у нас будут типы K скаляров и V векторов.

То есть тут у нас есть такие сущности:
– Типы элементов (например, скаляров и векторов), они образуют категорию с конечными (декартовыми) произведениями. Среди них выделенный тип “1” — нейтральный элемент произведений. Назовём эту категорию T, и в ней особо выделим проекции X ↠ Y (морфизмы, которые выделяют из произведения A × B ×···× D подпроизведение, скажем, B × C, и, опционально, меняют порядок аргументов).
– Типы предикатов P(x : T), где T какой-то тип элементов. Отношения суть предикаты на произведении нескольких элементарных типов отношений, например Id(p : T × T), а обыкновенные высказывания суть предикаты на 1. Если мы хотим чтобы у нас была логика первого порядка с равенством, то как раз постулируется что для каждого типа элементов автоматически есть предикат Id(x : T, y : T).
– Мы хотим, чтобы совокупность предикатов над одним и тем же типом была реализацией логики высказываний (т.е. категория предикатов над T была декартово замкнутой)
– Мы хотим, чтобы каждая проекция в категории элементов X ↠ Y порождала контравариантный функтор между категориями предикатов над Y и предиктов над X (это значит мы можем менять местами переменные у предикатов и добавлять переменные, которые никак не используются), сохраняющий структуру декартовой замкнутости.
— Далее мы хотим, чтобы у нас были кванторы — функторы сопряженные с вложениями слева и справа, соответственно предикаты P(x : X, y : Y) в предикаты (∀x,P)(y : Y) и (∃y,P)(y : Y). То есть мы уменьшаем количество переменных (можем уменьшить и до нуля, тогда получатся предикаты над единицей, то есть высказывания), замыкая убираемые переменные квантором всеобщности или существования.

Вот собственно и вся категорная семантика FOL, называются такие штуковины гипердоктринами (или, соответственно гипердоктринами с равенством, если требуются id-типы). Привожу определение по Pierre Clairambault, “From Categories with Families to Locally Cartesian Closed Categories”:

Screen Shot 2019-07-30 at 15.03.07

А вообще это классика, R. A. G. Seely, Hyperdoctrines, natural deduction, and the Beck condition, Zeitschrift für math. Logik und Grundlagen der Math., Band 29, 505-542 (1983).
ДР Цертуса 2011

О понятиях множества и класса

“Eine Menge ist eine Zusammenfassung bestimmter wohlunterschiedener Objekte unserer Anschauung
oder unseres Denkens — welche die Elemente der Menge genannt werden — zu einem Ganzen.”
— Georg Cantor, «Grundlagen einer allgemeinen Mannigfaltigkeitslehre»

(“Множество это собрание воедино определённых различимых объектов нашего представления или нашего мышления, называемых элементами множества.”)

§ О слове множество.

Когда говоришь про теории множеств, многие думают что там слово “множество” используется в обыденном смысле, как “множество всех молекул, из которых состоит стул”, но на самом деле речь совершенно не об этом.

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

Однако теория множеств, вошедшая в математику на столетие в качестве ассемблера, на который транслируют определения, построения и доказательства, это вполне конкретная теория множеств ZF(C) и её близкородственные вариации, называемые membership-based pure set theories. И они вообще говоря совершенно не о том, чтобы описать язык и поведение совокупностей объектов. Это о расширении логики первого порядка принципом рефлексии.Collapse )
ДР Цертуса 2011

Ещё одно введение в теории типов

В математике понятие “теория типов” развивается, и ещё непонятно в какой общности нужно будет давать определение. В контексте информатики теориями типов называют обобщения λ — просто типизированного лямбда-исчисления.

В сущности, теория типов — набор правил, которые позволяют конструировать выражения из подвыражений, в ситуации когда не любые выражений комбинируются, а только правильно стыкующиеся. Чтобы выразить “стыкуемость” вводится понятие типов (и набор правил, как эти типы записывать). Если терм x имеет тип T, пишут x : T. В λ всегда имеется какой-то набор базовых типов (например, тип Nat, содержащий все натуральные числа), и типы, получаемые из базовых X и Y путём применения оператора X -> Y.

После того как описано, какие бывают типы, можно записывать те самые правила конструирования выражений. Например:
  f : X -> Y    x : X
————————————––––––––––—
         f(x)


Для того, чтобы получившиеся выражения тоже можно было стыковать с чем-то дальше, в теорию типов добавляются дополнительные виды правил, как минимум требуется указать тип для любого сконструированного выражения:
  f : X -> Y    x : X
————————————––––––––––—
       f(x) : Y


Но в более сложных системах может хотеться, чтобы можно было применить f : X -> Y к такому x : X', что X и X' не совпадают “побуквенно”, но одно и то же по-существу (ну либо X' является подтипом X). Тогда нам нужны ещё правила конверсии типов, которые говорят в каких случаях X' ≼ X. Давайте предположим, что мы добавили в базовые типы нашего λ кроме самого Nat ещё типы Fin(n) дла каждого n : Nat, содержащие натуральные числа меньше n. То есть, у нас появились зависимые типы (такие операторы, которые превращают выражение какого-то фиксированного типа в тип, Fin(n) — как раз пример такого). Теперь нам хочется, чтобы туда, где требуется Fin(n) можно было подставить Fin(m), если n и m равны. То есть нам уже нужны правила равенства и для выражений. И правило, что если n = m, то Fin(n) ≼ Fin(m).

Существует два принципиально разных подхода к онтологии теорий типов — либо мы считаем, что есть некое данное свыше множество “сырых выражений” которые мы типизируем, либо мы вместе с типами задаём, какие выражения их населяют, с строим теорию снизу-вверх.

λ(Nat) и λ(Nat, Fin) можно сформулировать обоими способами. Можно сказать, что тип Nat состоит из лямбда-выражений
(\f ↦ (\x ↦ x))
(\f ↦ (\x ↦ f(x)))
(\f ↦ (\x ↦ f(f(x))))
...
А типы Fin(n) из нижних подмножеств этих выражений. Типы X -> Y, понятное, дело, тоже из лямбда-выражений. Тогда у нас, получается, любые типы состоят из лямбда-выражений, и для выражения любой “программы” не требуется ничего, кроме абстракции и применения. Между прочим, эта система типов позволяет записать в точности все рекурсивные функции, тотальность которых доказывается в арифметике первого порядка PA, и наоборот любому утверждению на языке арифметике первого порядка можно сопоставить функцию, определимую в этой теории типов, тотальность которой эквивалентна верности исходного утверждения. Можно также расширить λ(Nat, Fin) до λ×→(Nat, Fin) типом пар X × Y, и сказать что пара (x, y) это на самом деле лямбда-выражение (\f ↦ f(x)(y)). Всё ещё все типы населены только лямда-выражениями. Кстати, добавления типа пар добавляет λ только выразительности, но не силы — определимые там и там рекурсивные функции совпадают.

Такой подход называется PTS — Pure Type Systems. Активно разрабатываемая сейчас система Cedille показывается, что в рамках PTS можно сделать очень мощные системы типов, в частности включающие MLTT c Π, Σ и W-типами (более того, индексированными индуктивными типами), а ещё вероятно интенсиональными Id-типами (без UIP), но без вселенных и large elimination.

Можно, наоборот, сказать, что в λ(Nat) тип Nat состоит из особенных атомов Zero, Succ(Zero), Succ(Succ(Zero)) и т.д., и для них есть оператор паттерн-матчинга, а лямбда-выражения между двумя типами строятся индуктивно при помощи собственно конструкторов лямбда-выражений и операторов паттерн-матчинга. На этом пути, добавляя другие базовые типы и конструкторы типов мы тоже можем обобщать теорию без видимых пределов.
ДР Цертуса 2011

Разница между параметром и аргументом

Зависимые теории типов с иерархиями вселенных не позволяют говорить о вещах типа “категория всех групп”, они лишь позволяют говорить о “категориях всех U-малых групп”, проблема хорошо известная людям, занимающимся теорией категорий в теории множеств Тарского-Гротендика (ZFC + всякое множество содержится в какой-то вселенной Гротендика). Как в случае теории множеств, так и в случае теории типов есть сильные результаты, что утверждения для U-малых групп на самом деле переносятся на любой U', но чисто онтологически утверждения выглядят менее красиво, чем могли бы.

Для теорий множеств известен выход из этой неприятной ситуации. Для всякой теории множеств можно построить расширение, в котором можно говорить о классах (для ZFC оно называется NBG), тогда становится можно говорить о “категории всех групп”, но с ней ничего толком нельзя сделать, т.к. она класс, а не множество. Ну и можно построить теорию множеств вроде ZMC/S, добавив в ZFC принцип рефлексии, что есть такое множество U, являющееся вселенной Гротендика (т.е. моделью класса всех множеств), что любое утверждение 𝜑 равносильно утверждению 𝜑𝑈 (т.е. 𝜑 относительно U, синтаксической модификации утверждения 𝜑, где все классы заменили на соответствующие подмножества 𝑈).

Разумеется, хочется сделать такой же финт ушами и для теорий типов.

* * *


Вот рассмотрим f : ∀(T : *), T -> T. Это параметрическое семейство функций. Будучи специализированно для конкретного типа T, это функция T -> T.

В System F и её расширениях мы можем доказать, что всякое определимое семейство этого типа равно семейству idT = (\x : T) ↦ x.

В MLTT нет различия между параметром и аргументом. Путём введения типа Type («вселенной»), зависимость от параметра класса * представляется как зависимость от аргумента типа Type. То есть, idT типируется через (T : Type) -> T -> T. Благодаря отсутствию элиминаторов у вселенных, зависимость от аргумента типа Type остаётся в данном конкретном случае параметрической (“generic”, в частности мы не можем получить в указанном случае ничего кроме функции id, потому что не можем split by cases аргумент T — его тип Type не поддерживает spliting by cases и никакой другой интроспекции).

Проблема в том, что кроме интроспекции есть ещё один способ непараметрически использовать аргумент кроме интроспекции: его можно вернуть.

Терм (\T : Type) ↦ T имеет тип (T : Type) -> Type, и тут зависимость от T непараметрическая.

С точки зрения экспрессивности таким образом целесообразно иметь раздельно зависимые типы и оператор ∀. Тогда в подлежащей теории нужно уметь всё же говорить не только о типах, но и о классах (вообще их обычно называют kinds, но сейчас я предпочитаю такое название). Единственное использование классов именно в том, что когда мы пишем ∀(x : K) справа стоит не тип а класс. Блестящим такой теории является Cedille, причём там экспрессивность тамошних классов (замкнутость относительно зависимых сумм и произведений) как раз оправдывает использование слова “класс” — мы можем говорить о классе * всех типов, о классе всех групп и т.д.

Но при этом в Cedille нет large eliminations, а чтобы они там появились очень хочется пойти по пути ZMC/S и добавить просто какой-то сильнейший принцип рефлексии, который автоматически сгенерирует нам вселенные, с которыми удобно работать.

Вот например можно попробовать сказать, что у нас есть такой тип 𝑈 : *, и такая специальная метаоперация, которая превращает любое определение класса 𝜑 : 𝜅 в тип 𝜑𝑈 : *, путём замены в определении всех нужных * на 𝑈. Кстати, *𝑈 = 𝑈. А дальше какая-то схема правил, говорящая, что 𝜑𝑈 должно быть “малой” внутренней моделью 𝜑. Что-то типа метаоперации кодирования любого типового выражений класса 𝜑 в элементы 𝜑𝑈, и оператора декодирования в обратную сторону, но только это надо сделать как-то так аккуратно, чтобы не возникло противоречий. В частности, видимо, нужно чтобы композиция кодирования и декодирования давала не равенство, а изоморфизм. А невозможность прямого переноса терма вдоль изоморфизма предотвращала парадокс Расселла.
Очень мило, кстати, получается, что тут иерархия вселенных будет в другую сторону. * настоящая вселенная, *𝑈 = 𝑈 отражающая её “малая”, 𝑈𝑈 ещё более малая, и т.д.