Унивалентные основания математики. HoTT. Coq.

[arseniiv]

Xaositect в сообщении #1031904 писал(а):

Парадокс Жирара (Girard). Там нетривиально

Ого!

Xaositect в сообщении #1031904 писал(а):

Там в книжке кумулятивные универсумы, есть правило, по которому из $T:\mathcal{U}_i$ выводится $T:\mathcal{U}_{i+1}$.

Да, получается, правило транзитивности и не нужно. Смотрел, главное, на то правило (они же на одной строке) и чего-то не высмотрел. Хотя всё равно не получится так, что все универсы $\mathcal U_i,\ldots,\mathcal U_{i+k}$ будут друг в друге, хотя получится $\mathcal U_{i+k}\colon\mathcal U_{i+j},0\leqslant j\leqslant k$ — как понимаю, этого уже достаточно для получения упомянутого вами парадокса?

[Yorick]

Есть следующие вопросы, буду рад, если разбирающиеся люди ответят или укажут направление, если решение слишком объемно.

Я напишу текст как я понимаю некоторые моменты(в которых я сомневаюсь), и если в этом будет ошибка - надеюсь это заметят. Отмечу: "формеры" - калька с "type formers", ведь "знакоопределенность" - это свойство не конкретного типа, а его формера, т.е. вида, хоть в книге и пишут positive/negative types.

Cуществует классификация видов типов: положительные формеры(+), негативные формеры($\Sigma, \Pi, \mathcal{U}$) и отдельный случай(=-тип, но по сути он положительный). Характерная черта всех отрицательных формеров - то, что они, формируя новый тип из типов которые являются явными высказываниями(mere propositions), передают это свойство новому типу.

Вопрос: как же по правилам для типов понять, что он, например, отрицательный? Ответ: Произвольный формер - положительный, если не доказано обратное.
Что он отрицательный доказывается яным определением всех путей в новом типе через пути в исходных типах.(через элементы - наверное тоже?)

Хорошо. Теперь вспомним про ограничения для конструкторов индуктивных типов. Для простых индуктивных типов это требование "строгой положительности", т.е. для некоторого вида Q они такие(согласно hott book): конструктор - это функция с неотрицательным целым числом аргументов, причём её кодомен - это $Q(A_1,...,A_n)$. $(1)\rightarrow(2)\rightarrow(3)\rightarrow...\rightarrow Q$. А на месте цифр 1,2,3 либо функции с кодоменом $Q(A_1,...,A_n)$ и аргументов типа $Q(A_1,...,A_n)$ они не принимают, либо типы не равные $Q(A_1,...,A_n)$ по определению.

То есть фактиески - мы рассматриваем все возможные "разделения" аргументов по скобкам, причем вложенных скобок нет. И каждая скобка не содержит Q только один раз - в самой правой позиции или вовсе его не содержит.
Однако это определение пропускает невалидный конструктор $g: Q \rightarrow \mathcal N \rightarrow Q$
Возникает вопрос: как улучшить определение? Возможна ли такая конструктивная в обоих смыслах рекурсия:
Кандидат - функция с кодоменом $Q(A_1,...,A_n)$, и неотрицательным числом аргументов, которые тоже являются кандидатами.
Конструкторы вида Q - это набор пар (название, функция-кандидат).

Сказано необходимое условие: функтор из некоторого типа X в домен конструктора должен быть ковариантным.
Мне непонятно, почему это отображение назвали функтором, например, для $inl:A\rightarrow A+B$ какую структуру сохраняет отображение $\lambda(X:\mathcal{U}).A$?

Насколько я понял, recursion priniple для каждого формера, это частный случай induction principle.
Индукцию для каждого формера, поняв её, можно выразить в короткой фразе, описывающую элиминацию, например:
0) Любое утверждение верно, если ноль имеет элемент.
1) Всё, что верно для $\star : 1$, верно и для любого $s : 1$.
2) Что верно для всех элементов A и B в отдельности, то верно и для их пар.
3) Утверждение, верное для некого элемента A или для некого элемента B, верно и для некоторого элемента A+B
4) Доказав тождественное равенство некоторых двух утверждений при условии стягивания пропозиционально равных элементов в тождественно равные - мы доказали пропозиционное равенство исходных утверждений.
и т.д.
Так вот: Как звучит индукция для $\mathcal{S}^1$? Хотя скорее более важно - как она звучит для suspensions(т.е. $\Sigma$)?

И пара коротких вопросов из другой области:
1)Вроде универсум не является множеством. Есть ли что-то более маленькое, что тоже не является множеством. Есть ли своего рода truncation, только не до mere proposition, a до n-типа, например, в частности, до множества?
2)Если транспортировать доказательство утверждения по разным путям, но в одну и ту же точку, то может ли измениться пункт назаначения доказательства? (трудно придумать пример)
3)Известно, что $\Sigma 0 \simeq 2 $ и $\Sigma 2 \simeq \mathcal{S}^1 $. Тогда получается, что $\mathrm N : \mathcal{S}^1$ и $\mathrm S : \mathcal{S}^1$, однако, afaik, в $\mathcal{S}^1$ только base. по каким причинам тут не работает тот же аргумент, что и для $0_2 \neq 1_2$?

И последнее, но самое нужное:
Есть некий, уже сформулированный, сложный тип, и надо проверить его населённость.
Можно кратко обозначить pros and cons Coq и Agda (Epigram, Haskell, ...), если предстоит выбирать на чём реализовывать этот тип.
Какие есть ограничения? Какая библиотека hott для этих языков лучше развита? Наверняка это всё описывалось, только вот где?