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

[Yorick]

Есть замечательная книга, которую можно бесплатно скачать отсюда:
http://homotopytypetheory.org/book/
(28(!!) человек её писали, в том числе Мартин-Лёф, Кокан и Воеводский)

Моя цель:
изучить полностью хотя бы первую главу книги.
решить упражнений в конце главы с помощью формальной системы в приложении "A2 The second presentation" на стр.537

Мотивация:
1) очень широкий круг математических объектов возможно будет аксиоматизировать и лучше понимать
2) напрямую это связано с машинной проверкой теорем (язык Сoq)

Проблема:
Никто из знакомых мне математиков не занимается этим.

Вопросы:

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

Пример: ассоциативность композиции - элементарна на бумаге
$(f \circ (g\circ h))(x)=f((g\circ h)(x))=f(g(h(x)))=(f\circ g)(h(x))=((f\circ g)\circ h)(x)$,
но как её осуществить через ту формальную систему?
Далее тип функции композиции:
$\circ : \Pi_{A,B,C:U_0} (A \rightarrow B) \rightarrow (B \rightarrow C) \rightarrow(A \rightarrow C) $
Учитывая, что по определению
$(A \rightarrow B) \equiv \Pi_{a:A} B $
$\Pi_{x_1,x_2:X} Y \equiv \Pi_{x_1:X}\Pi_{x_2:X} Y$, то можно перейти к совершенно страшной формуле со множество букв $\Pi$ .

Определяем композицию как
$\circ(g, h, x) := g(h(x))$

Вопрос 1: как это всё в формальном виде написать в контекст Г?
(контекст как я понял - просто список утверждений)

Вопрос 2: Как, используя описанные в А2 правила подстановки доказать ассоциативность композиции?
(в Википедии есть доказательство на Coq, но оно пока вне моего понимания, не могу связать с формальной системой, описанной в книге)

Вопрос 3: Кто-нибудь этим занимается или хочет(а это, полагаю, очень круто для развития своего математического аппарата) заняться за компанию?

Вопрос 4: Можно привести любые(желательно побольше) простые содержательные пример, когда мы что-то определеяем в этой системе, но не отступаем от её строгости.

Заранее спасибо.

[Xaositect]

Я читал HoTT поверхностно, сейчас тоже хочу подробно проработать, но времени нет.

Композицию с тем типом, который Вы указали, можно определить в пустом контексте как $\circ = \lambda (A, B, C : \mathcal{U}) .\, \lambda (g : A\to B) .\, \lambda (h : B\to C) .\, \lambda (x : A) .\, h(g(x))$. Получить это можно, применяя правила $\Pi$-elim и $\Pi$-intro из контекста $A,B,C : \mathcal{U}, g : A\to B, h : B\to C, x : A$. Если все расписывать, то получится вот так:

1. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C, x : A\ \mathrm{ ctx}$
2. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C, x : A \vdash x : A$ (из 1, правило Vble)
3. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C, x : A \vdash g : A\to B$ (из 1, правило Vble)
4. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C, x : A \vdash g(x) : B$ (из 2 и 3, правило $\Pi$-elim с учетом определения $A\to B = \Pi (x : A). B$)
5. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C, x : A \vdash h : B\to C$ (из 1, правило Vble)
6. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C, x : A \vdash h(g(x)) : C$ (из 5 и 6, правило $\Pi$-elim с учетом определения $B\to C = \Pi (x : B). C$)
7. $A : \mathcal{U}, B : \mathcal{U}, C : \mathcal{U}, g : A\to B, h : B\to C \vdash \lambda (x:A).h(g(x)) : A\to B$ (из 6, правило $\Pi$-intro с учетом определения $A\to C = \Pi (x : A). C$)
и так далее, с помощью $\Pi$-intro вводим кучу лямбд, в итоге получаем
$\vdash \lambda (A {:} \mathcal{U}).\lambda (B {:} \mathcal{U}). \lambda (C {:} \mathcal{U}) .\, \lambda (g : A\to B) .\, \lambda (h : B\to C) .\, \lambda (x : A) .\, h(g(x)) : \Pi (A : \mathcal{U}). \Pi (B : \mathcal{U}). \Pi (C : \mathcal{U}). (A\to B) \to ((B\to C) \to (A\to C))$

Дальше с помощью $\circ(A, B, C, g, h, x) \equiv h(g(x)) : C$ (это равенство доказывается многократным применением $\Pi$-comp), Subst и $\Pi$-uniq можно доказать ассоциативность.

В общем, это долго и нудно, такими вещами пусть занимаются компьютеры. Если хотите заниматься формализованными вещами, лучше разберитесь с coq или agda.

[Yorick]

Планирую, чтобы разобраться:
а) написать доказательство полностью и строго
б) постепенно писать программу для вывода выражений.(уже немного автоматизировал процесс: см. код сообщения. Код данного сообщения виден, если его цитировать)

Вопросы:
1) что-нибудь не нравится в приведённом ниже коде? (Я не использовал Vble; номера используемых строк в скобках, в порядке записи "числителя" правил в книге; def значит заданы изначально в контексте Г)

2) в правиле П-form для вывода необходимо существование в контексте Г семейства типов "из A в U". По-простому - множество функций. Как получить такое(см строки 4 и 5) выражение(терм)? По-моему необходимо просто существование элемента в A и существование множества в U, например самого А.
Я не понимаю, в чём сокровенный смысл именно такой записи через запятую. (Почему нельзя просто сделать так:
$A:U_i$
$B:U_{i+1\mbox{(правильно?)}}$
$a:A$ (т.е. типы непустые)
$b:B$,
следовательно существует П-тип $\Pi(x:A)B:U_i$)

\def\mylan#1{\newcounter{myl#1}} \def\myit{\stepcounter{mya}\arabic{mya}} \def\myla#1{\setcounter{myl#1}{\value{mya}}} \newcounter{mya} \mylan{1}\mylan{2}\mylan{3}\mylan{4} \begin{tabular}{llclcp{6cm}} %\mys{\Gamma,x:A,ctx-EMP} %%\\ %\myit & \mbox{ctx-EMP}&$=>$& $\Gamma \vdash A:U_0$\\ \myit & def &$\Rightarrow$& $\Gamma$&$\vdash$&$ A:U_0$\myla{1}\\ \myit & def &$\Rightarrow$& $\Gamma$&$\vdash$&$ B:U_0$\\ %\setcounter{myl1}{\value{mya}} \myit & def &$\Rightarrow$& $\Gamma$&$\vdash$&$ C:U_0$\\ %\myla , \myit & def? &$\Rightarrow$& $\Gamma , x:A $&$\vdash$&$ B:U_0$\myla{2}\\ \myit & def? &$\Rightarrow$& $\Gamma , x:A $&$\vdash$&$ C:U_0$\myla{4}\\ \myit & $\Pi$-$form(\arabic{myl1},\arabic{myl2})$&$\Rightarrow$& $\Gamma$&$\vdash$&$ \Pi(a:A).B:U_0$\\ \myit & $\Pi$-$form(\arabic{myl1},\arabic{myl4})$&$\Rightarrow$& $\Gamma$&$\vdash$&$ \Pi(a:A).C:U_0$\\ \myit & def &$\Rightarrow$& $\Gamma$&$\vdash$&$ x:A$\myla{1}\\ \myit & def &$\Rightarrow$& $\Gamma$&$\vdash$&$ g:\Pi(a:A).B$\myla{3}\\ \myit & $\Pi$-$elim(\arabic{myl3},\arabic{myl1})$ &$\Rightarrow$& $\Gamma$&$\vdash$&$ g(x):B$\myla{1}\\ \myit & def &$\Rightarrow$& $\Gamma$&$\vdash$&$ h:\Pi(a:B).C$\myla{3}\\ \myit & $\Pi$-$elim(\arabic{myl3},\arabic{myl1})$ &$\Rightarrow$& $\Gamma$&$\vdash$&$ h(g(x)):B$\myla{3}\\ \myit & $\Pi$-$intro(\arabic{myl3})$ &$\Rightarrow$& $\Gamma$&$\vdash$&$ \lambda(z:A).h(g(z)):\Pi(a:A).C$\myla{3}\\ ...\\ ?& ? &$\Rightarrow$& $\Gamma$&$\vdash$&$ \lambda(A:U_0).\lambda(B:U_0).\lambda(C:U_0).\lambda(z:A).h(g(z)):\Pi(a:A).C$\\ $?& ? &$\Rightarrow$& $\Gamma$&$\vdash$& $\circ(A, B, C, g, h, x) \equiv h(g(x)) : C$ \\ \end{tabular}
Спасибо.

[arseniiv]

Строку, например, 4 можно получить так:

$$\frac{\Gamma\vdash A:\mathcal U_0\quad\quad\Gamma\vdash B:\mathcal U_0}{\Gamma,x:A\vdash B:\mathcal U_0}\;\mathsf{Wkg}_1$$

из ваших гипотез 1 и 2. Только зачем вам гаммы? Гамма — это метатеоретическое обозначение контекста; в конкретном выводе и контексты конкретные. Хотя можно, конечно, сразу «схемы выводов» делать, только я пока не вижу плюсов, кроме как производные правила вывода получать.

-- Пт янв 23, 2015 22:45:24 --

Yorick в сообщении #967222 писал(а):

Я не понимаю, в чём сокровенный смысл именно такой записи через запятую. (Почему нельзя просто сделать так:
$A:U_i$
$B:U_{i+1\mbox{(правильно?)}}$
$a:A$ (т.е. типы непустые)
$b:B$,
следовательно существует П-тип $\Pi(x:A)B:U_i$)

Не понял вопрос, но спрошу о другом: разве тип $\Pi(x:\mathbf0).\mathbf1$ не существует и не содержит элемент $\lambda(x:\mathbf0).\star$? Для образования Π-типа наличие элементов в типе аргумента функции не обязательно!

[Yorick]

Вопросы:
1) В определении композиции я использую "вселенную" $\mathcal{U}_i$, однако уже в $\mathcal{U}_{i+1}$ могут быть множества(они же типы), для которых не определена композиция. Как тогда её определять в общем случае для всех юнивёрсумов?
2) Допустимо ли следующее применение правила П-comp? И как тогда понимать замену $\mathcal{U}_0[x/z]$?

$$(1)\Gamma, z:A \vdash B:\mathcal{U}_0$$\\ $$(2)\Gamma \vdash x:A$$\\ $$(3)\Pi-comp(\myr{1},\myr{2}) \Rightarrow \Gamma \vdash (\lambda(z:A).B)(x)\equiv B[x/z]:\mathcal{U}_0[x/z]$$

3) Я правильно понял, что формальная система, описанная в книге - творчески переработанный Мартин-Лёф и поэтому маловероятно найти более подробное её рассмотрение? (в библиографии пока не нашёл)
4) Что означает правило ctx-emp?
5) Как понимать точки в правилах $\Sigma-elim$ и $\Sigma-comp$? Похоже на лямбда-абстракции.
Книга говорит:

Цитата:

The expression $\Sigma(x:A).B$ binds free occurrences of x in B. Furthermore,
because $ind_{\Sigma(x:A).B}$ has some arguments with free variables beyond those
in Г, we bind (following the variable names above) z in C, and x and y
in g. These bindings are written as z.C and x.y.g, to indicate the names
of the bound variables. In particular, we treat $ind_{\Sigma(x:A).B}$ as a primitive,
two of whose arguments contain binders; this is superficially similar to,
but different from, $ind_{\Sigma(x:A).B}$ being a function that takes functions as ar-
guments.

(раздел A.2.5)

6*) В доказательстве ниже есть грубые логические ошибки?

Ниже, в утверждении 20 - решётка(#) обозначает, нужный для использования данного правила терм находится в "посыле" , т.е. до символа $\vdash$. (Кстати, как он называется?)

Определение композиции:
\def\mylan#1{\newcounter{myl#1}\setcounter{myl#1}{0}} \def\myit{\stepcounter{mya}\arabic{mya}} \def\myla#1{\setcounter{myl#1}{\value{mya}}} \def\GammKI{\Gamma} \def\Un\mathcal{U} \newcounter{mya}\setcounter{mya}{0} \mylan{1}\mylan{2}\mylan{3}\mylan{4}\mylan{5}\mylan{6}\mylan{7}\mylan{8}\mylan{9}\mylan{10} \mylan{11}\mylan{12}\mylan{13}\mylan{14}\mylan{15}\mylan{16}\mylan{17}\mylan{18}\mylan{19}\mylan{20} \mylan{21}\mylan{22}\mylan{23}\mylan{24}\mylan{25}\mylan{26}\mylan{27}\mylan{28}\mylan{29}\mylan{30} \mylan{31}\mylan{32}\mylan{33}\mylan{34}\mylan{35}\mylan{36}\mylan{37}\mylan{38}\mylan{39}\mylan{30} \begin{tabular}{llclcp{7cm}} \myit & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ A:\mathcal{U}_0$\myla{1}\\ \myit & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ B:\mathcal{U}_0$\myla{2}\\ %\setcounter{myl1}{\value{mya}} \myit & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ C:\mathcal{U}_0$\myla{3}\\ \myit & $wkg_1(1,2)$ &$\Rightarrow$& $\GammKI, z:A $&$\vdash$&$ B:\mathcal{U}_0$\myla{4}\\ \myit & $wkg_1(1,3)$ &$\Rightarrow$& $\GammKI, z:A $&$\vdash$&$ C:\mathcal{U}_0$\myla{5}\\ \myit & $wkg_1(2,3)$ &$\Rightarrow$& $\GammKI, z:B $&$\vdash$&$ C:\mathcal{U}_0$\myla{6}\\ \myit & $\Pi$-$form({1},{4})$&$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(w:A).B:\mathcal{U}_0$\myla{7}\\ \myit & $\Pi$-$form({1},{5})$&$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(w:A).C:\mathcal{U}_0$\myla{8}\\ \myit & $\Pi$-$form({2},{6})$&$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(w:B).C:\mathcal{U}_0$\myla{9}\\ \myit & $wkg_1({1},{8})$ &$\Rightarrow$& $\GammKI, f:\Pi(z:B).C$&$\vdash$&$ \Pi(z:A).C :\mathcal{U}_0$\myla{10}\\ \myit & $\Pi$-$form({9},{10})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{11}\\ \myit & $wkg_1({7},{11})$ &$\Rightarrow$& $\GammKI, g:\Pi(z:A).B$&$\vdash$&$ \Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{12}\\ \myit & $\Pi$-$form({7},{12})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{13}\\ \myit & $wkg_1({3},{13})$ &$\Rightarrow$& $\GammKI, C:\mathcal{U}_0$&$\vdash$&$ \Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{14}\\ \myit & $\Pi$-$form({3},{14})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{15}\\ \myit & $wkg_1({2},{15})$ &$\Rightarrow$& $\GammKI, B:\mathcal{U}_0$&$\vdash$&$ \Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{16}\\ \myit & $\Pi$-$form({2},{16})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(B:\mathcal{U}_0).$\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{17}\\ \myit & $wkg_1({3},{17})$ &$\Rightarrow$& $\GammKI, A:\mathcal{U}_0$&$\vdash$&$ \Pi(z:A).C :\mathcal{U}_0$\myla{18}\\ \myit & $\Pi$-$form({3},{18})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ \Pi(A:\mathcal{U}_0).\Pi(B:\mathcal{U}_0).$\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C :\mathcal{U}_0$\myla{19}\\ %A.3 p545 \end{tabular}
\def\myit{\stepcounter{mya}\arabic{mya}} \def\myla#1{\setcounter{myl#1}{\value{mya}}} \def\GammKI{\Gamma} \def\Un\mathcal{U} \newcounter{mya}\setcounter{mya}{19} \begin{tabular}{llclcp{7cm}} \myit\myla{20} & $\Pi$-$elim({4}, \mbox{\#})$ &$\Rightarrow$& $\GammKI, z:A $&$\vdash$& $g(z):B$\\ \myit\myla{21} & $\Pi$-$elim({6}, \mbox{20})$ &$\Rightarrow$& $\GammKI, z:A $&$\vdash$& $h(g(z)):C$\\ \myit & $\Pi$-$intro({21})$ &$\Rightarrow$& $\GammKI $&$\vdash$& $\lambda(z:A).h(g(z)):\Pi(z:A).C$\myla{22}\\ \myit & $\Pi$-$wkg({10},{22})$ &$\Rightarrow$& $\GammKI, f:\Pi(a:B).C $&$\vdash$&$\lambda(z:A).h(g(z)):\Pi(z:A).C$\myla{23}\\ \myit & $\Pi$-$intro({23})$ &$\Rightarrow$& $\GammKI $&$\vdash$& $\lambda(f:\Pi(a:B).C).\lambda(z:A).h(g(z)): $\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{24}\\ \myit & $\Pi$-$wkg({12},{24})$ &$\Rightarrow$& $\GammKI, g:\Pi(a:A).B$&$\vdash$&$\lambda(f:\Pi(a:B).C).\lambda(z:A).h(g(z)):$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{25}\\ \myit & $\Pi$-$intro({25})$ &$\Rightarrow$& $\GammKI $&$\vdash$& $\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)): $\\&&&&&$\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{26}\\ \myit & $\Pi$-$wkg({3},{26})$ &$\Rightarrow$& $\GammKI, C:\mathcal{U}_0$&$\vdash$&$\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)):\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{27}\\ \myit & $\Pi$-$intro({27})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ \lambda(C:\mathcal{U}_0).\\ &&&&&\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)): $\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{28}\\ \myit & $\Pi$-$wkg({2},{28})$ &$\Rightarrow$& $\GammKI, B:\mathcal{U}_0$&$\vdash$&$\lambda(C:\mathcal{U}_0).\\ &&&&&\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)): $\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{29}\\ %A:\mathcal{U}_0 \myit & $\Pi$-$intro({29})$ &$\Rightarrow$& $\GammKI $&$\vdash$&$ \lambda(B:\mathcal{U}_0).\lambda(C:\mathcal{U}_0).\\ &&&&&\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)): \Pi(B:\mathcal{U}_0).$\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{30}\\ \myit & $\Pi$-$wkg({1},{30})$ &$\Rightarrow$& $\GammKI, A:\mathcal{U}_0$&$\vdash$&$ \lambda(B:\mathcal{U}_0).\lambda(C:\mathcal{U}_0).\\ &&&&&\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)): \Pi(B:\mathcal{U}_0).$\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\myla{31}\\ \myit & $\Pi$-$intro({31})$ &$\Rightarrow$& $\GammKI$&$\vdash$&$ \circ \equiv \lambda(A:\mathcal{U}_0).\lambda(B:\mathcal{U}_0).\lambda(C:\mathcal{U}_0).\\ &&&&&\lambda(g:\Pi(a:A).B).\lambda(f:\Pi(a:B).C).$\\&&&&&$\lambda(z:A).h(g(z)): \Pi(A:\mathcal{U}_0).\Pi(B:\mathcal{U}_0).$\\&&&&&$\Pi(C:\mathcal{U}_0).\Pi(g:\Pi(a:A).B).$\\&&&&&$\Pi(f:\Pi(a:B).C).\Pi(z:A).C$\\ %A.3 p545 \end{tabular}

[arseniiv]

Yorick в сообщении #968299 писал(а):

Ниже, в утверждении 20 - решётка(#) обозначает, нужный для использования данного правила терм находится в "посыле" , т.е. до символа $\vdash$.

Таким способом это не работает. Можно выводить только из того, что выше, тем более что контекст не является утверждением.

Yorick в сообщении #968299 писал(а):

(Кстати, как он называется?)

Да вроде просто контекст (context), посмотрите A.2.1.

Yorick в сообщении #968299 писал(а):

1) В определении композиции я использую "вселенную" $\mathcal{U}_i$, однако уже в $\mathcal{U}_{i+1}$ могут быть множества(они же типы), для которых не определена композиция. Как тогда её определять в общем случае для всех юнивёрсумов?

Ровно так же, меняя индексы у $\mathcal U_i$ на нужные (в конкретном выводе все универсумы имеют конкретные индексы, а если там везде $i+k$, то это уже схема, генерирующая по выводу для каждого конкретного $i$ с соответствующими разницами во встречающихся типах).

Yorick в сообщении #968299 писал(а):

2) Допустимо ли следующее применение правила П-comp? И как тогда понимать замену $\mathcal{U}_0[x/z]$?

$$(1)\Gamma, z:A \vdash B:\mathcal{U}_0$$

$$(2)\Gamma \vdash x:A$$

$$(3)\Pi-comp(\myr{1},\myr{2}) \Rightarrow \Gamma \vdash (\lambda(z:A).B)(x)\equiv B[x/z]:\mathcal{U}_0[x/z]$$

Если я сравнил аккуратно, то всё в порядке. А $\mathcal{U}_0[x/z]$ — это просто $\mathcal U_0$, т. к. переменная $z$ в терме $\mathcal U_0$ не встречается.

Yorick в сообщении #968299 писал(а):

4) Что означает правило ctx-emp?

Это правило утверждает, что пустой контекст — это контекст. Без него нельзя было бы вывести никакое утверждение вида $\vdash a:A$ или $\vdash a\equiv b:A$, и, кроме того, без изменений в правилах вывода, вообще никакое утверждение, т. к. не к чему было бы применять ctx-EXT.

Yorick в сообщении #968299 писал(а):

5) Как понимать точки в правилах $\Sigma-elim$ и $\Sigma-comp$?

Эти точки указывают, что некоторые переменные терма, не связанные другим образом ($\lambda,\Pi,\Sigma$), связаны, чтобы подстановка вместо одноимённой переменной их не заменяла.

[alex_dorin]

Не обязательно использовать Coq. Можно использовать DFG, TPTP и пруверы первопорядковой логики и получать доказательства.

[Yorick]

Вот, допустим такой лист выкладок
\def\GammKI{\Gamma} \begin{tabular}{llclcp{7cm}} 1 & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ A:\mathcal{U}_0$\\ 2 & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ B:\mathcal{U}_0$\\ 3 & $wkg_1(1,2)$ &$\Rightarrow$& $\GammKI, z:A$&$\vdash$&$ B:\mathcal{U}_0$\\ 4 & $\Pi-form(1,3)$ &$\Rightarrow$& $\GammKI$&$\vdash$&$\Pi(z:A).B:\mathcal{U}_0$\\ \end{tabular}$$

Что значит выражение $\Gamma, z:A \vdash B:\mathcal{U}_0$ в интерпретации теории множеств?
(Я понимаю как "в контексте гамма существует правило под названием B, которое сопоставляет каждому элементу z множества A подмножество множества U". Правда пока не совсем ясно как это правило записывать)

$$a:A,\quad A:\mathcal{U}_0,\quad \mathcal{U}_0:\mathcal{U}_1, ...$$

"Вселенная" это тоже тип или между ними есть разница? Вроде тоже тип, просто другого уровня: элемент 'a' - тип 1го уровня. множество 'A' - 2го, вселенная 'U' - 3го.

arseniiv в сообщении #968363 писал(а):

Yorick в сообщении #968299 писал(а):

4) Что означает правило ctx-emp?

Это правило утверждает, что пустой контекст — это контекст. Без него нельзя было бы вывести никакое утверждение вида $\vdash a:A$ или $\vdash a\equiv b:A$, и, кроме того, без изменений в правилах вывода, вообще никакое утверждение, т. к. не к чему было бы применять ctx-EXT.

Но что такое пустой контекст?(типа некого глобального, берущийся по умолчанию?) Мне кажется, что уместно делать несколько контекстов, называть их Г1, Г2, ..., ГN, и при каком-либо доказательстве "подключать" их, используя

$$\frac{\Gamma\vdash a:A \quad \Gamma,x:A,\Delta\vdashb:B}{\Gamma,\Delta\lbrack a/x \rbrack\vdash b\lbrack a/x \rbrack : B \lbrack a/x \rbrack}Subst_1,$$

где заменяются те переменные, которые объявлялись как "def".

В чём разница между positive type и negative type?

Буду благодарен за названия хороших источников(желательно русскоязычных, но не обязательно), по которым можно изучать основы этой теории типов.

p.s.
исправления в мой последний большой текст(я пока очень не уверен в них)
\def\GammKI{\Gamma} \begin{tabular}{llclcp{7cm}} 0 & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ \mathcal{U}_0$ //или несколько для общего случая?\\ 3.5 & def &$\Rightarrow$& $\GammKI$&$\vdash$&$ w:A$\\ 20 & $\Pi$-$elim({4}, {3.5})$ &$\Rightarrow$& $\GammKI, z:A$&$\vdash$& $g(z):B$\\ 21 & $\Pi$-$elim({6}, {20})$ &$\Rightarrow$& $\GammKI, z:A$&$\vdash$& $h(g(z)):C$\\ \end{tabular}

p.p.s.
https://github.com/pcapriotti/hott-exercises
http://blog.ezyang.com/2013/07/hott-exe ... -progress/
к сожалению предлагаемые решения упражнений на Agda и Coq не показывают как сам механизм работает, я бы с удовольствием почитал какие-нибудь машинные выводы, чтобы яснее видеть механизм.

[Xaositect]

Yorick в сообщении #1016364 писал(а):

Что значит выражение $\Gamma, z:A \vdash B:\mathcal{U}_0$ в интерпретации теории множеств?

Начнем с того, что у HoTT интерпретации в теории множеств, как я понимаю, нет. Из-за нетривиальности равенства и из-за универсумов. Но если Вам хочется какую-то интуицию из теории множеств, то можно считать, что типы в $U_0$ - это "нечто типа множеств", а типы в $U_1$ - это "нечто типа классов". Соответственно, интерпретация $\Gamma, z\colon A \vdash B\colon U_0$ будет "в контексте $\Gamma$ каждому элементу "множества" $A$ сопоставляется "множество" $B$".

Yorick в сообщении #1016364 писал(а):

"Вселенная" это тоже тип или между ними есть разница?

Тоже тип. Просто элементами его являются типы, а так ничего особенного.

Yorick в сообщении #1016364 писал(а):

Но что такое пустой контекст?(типа некого глобального, берущийся по умолчанию?)

Пустой контекст - это пустой контекст. Это значит, что мы ничего не предполагаем. Например, $\vdash \lambda (A\colon U_0). \lambda (a\colon A). a \colon \Pi (A\colon U_0). (A\to A)$ значит, что у нас есть конкретный обитатель конкретного типа, и нам никаких предположений для этой конструкции не надо.

[arseniiv]

Yorick в сообщении #1016364 писал(а):

Буду благодарен за названия хороших источников(желательно русскоязычных, но не обязательно), по которым можно изучать основы этой теории типов.

Основа, как указывается в самой книге HoTT (Introduction § Type theory) — это теория типов Мартина-Лёфа (интенсиональная, если будет выбор между ей и экстенсиональной), так что если видели книги по этой, могут сгодиться (пока там к аксиомам не прибавляют что-нибудь не выводимое при добавлении вместо этого унивалентности, конечно).

[Yorick]

Зачем нужно правило 0-Elim и $\mbox{ind}_\mathbf{0}$? У нулевого типа нет элемента, соответственно никогда этим правилом воспользоваться не сможем.

Цитата:

The induction principle for the empty type
$\mbox{ind}_\mathbf{0}:\limits\Pi_{(C:\mathbf{0}\rightarrow\mathcal{U})}\limits\Pi_{(z:\mathbf{0})}C(z)$
gives us a way to define a trivial dependent function out of the empty
type(?).

Как доказать, что $\mathcal{U}_{\infty}:\mathcal{U}_{\infty}$ неверно и приводит к заселению типа 0?

Если принять, что:
$A:\mathcal{U}_i$,
$a,b:A$,
то почему следующий тип уже не может принадлежать $\mathcal{U}_i$?
$\left(\limits\Pi_{P:A\rightarrow \mathcal{U}_i} P(a) \rightarrow P(b)\right):\mathcal{U}_{i+1}$
(как прийти к противоречию?)

Предположнение: Если $A:\mathcal{U}_i$ и ... , то тип типа $\mbox{ind}_\Sigma$ принадлежит $\mathcal{U}_{i+1}$, но не $U_i$?

Что можно сказать про тип $(A\rightarrow \mathbf{0})\times((A\rightarrow \mathbf{0}) \rightarrow \mathbf{0})$?
Населён или не населён, если теория типов consistent?
Населён или не населён, если теория типов inconsistent?

p.s. Есть ли примеры необходимости отсутсвия унивалентности какой-либо вселенной для корректного описания какого-либо объекта математики, изначально не относившегося напрямую к теории типов?

[arseniiv]

Yorick в сообщении #1019111 писал(а):

Как доказать, что $\mathcal{U}_{\infty}:\mathcal{U}_{\infty}$ неверно и приводит к заселению типа 0?

А что такое $\mathcal U_\infty$? Насколько помню, универсы нумеруются только натуральными числами.

Yorick в сообщении #1019111 писал(а):

Зачем нужно правило 0-Elim и $\mbox{ind}_\mathbf{0}$? У нулевого типа нет элемента, соответственно никогда этим правилом воспользоваться не сможем.

Как же не сможем? Всё, что мы можем вывести без посылки $x:\mathbf0$, мы сможем вывести и с ней. Вот попробуйте вывести recursor $\mathsf{rec}_{\mathbf0}:\Pi(A:\mathcal U).\,\mathbf0\to A$ с помощью этого правила и правила $\Pi$-\textsc{intro}. Он должен получиться равен $\lambda(A:\mathcal U).\,\lambda(y:\mathbf0).\mathsf{ind}_{\mathbf0}(x.\,A,y)$.

[Yorick]

Цитата:

The following important principles, called substitution and weak-
ening, need not be explicitly assumed. Rather, it is possible to show, by
induction on the structure of all possible derivations, that whenever the
hypotheses of these rules are derivable, their conclusion is also deriv-
able.

Каким образом строго доказываются утверждения по индукции на структуре всех возможных выводов?(например, $wkg_1$)

Цитата:

А что такое $\mathcal U_\infty$? Насколько помню, универсы нумеруются только натуральными числами.

Я просто хочу увидеть как прийти к противоречию из утверждения, что в неком унивёрсуме содержатся все типы, включая его самого.

[arseniiv]

А что, это обязательно должно привести к противоречию? Ничего такого про универсумы там не было введено. В изложении мог что-нибудь пропустить или уже забыть, но это необходимо должно быть в начале первой части, большую часть которой я прочитал один раз. Утверждение $\mathcal U_{i+k}\colon\mathcal U_i$ даже не «склеивает» универсумы $\mathcal U_i,\ldots,\mathcal U_{i+k}$, делая находящиеся в них наборы типов одинаковыми, и даже не помещает каждый из них в каждый, потому что нет никакого «правила транзитивности» $\mathcal U_i\colon\mathcal U_j,\mathcal U_j\colon\mathcal U_k\vdash\mathcal U_i\colon\mathcal U_k$. Уж тем более нет каких-то следствий посерьёзнее, в том числе для универсумов с $i+k+1$. Если что-то упускаю, поправляйте.

Если никто не напишет по первому вопросу, соберусь.

P. S. Ерунда с формулами поправлена.

[Xaositect]

arseniiv в сообщении #1031889 писал(а):

А что, это обязательно должно привести к противоречию?

Парадокс Жирара (Girard). Там нетривиально, Yorick, почитайте где-нибудь описание этого парадокса.

arseniiv в сообщении #1031889 писал(а):

Утверждение $\mathscr U_{i+k}\colon\mathscr U_i$ даже не «склеивает» универсумы $\mathscr U_i,\colon\mathscr U_{i+k}$, делая находящиеся в них наборы типов одинаковыми, и даже не помещает каждый из них в каждый, потому что нет никакого «правила транзитивности» $\mathscr U_i\colon\mathscr U_j,\mathscr U_j\colon\mathscr U_k\vdash\mathscr U_i\colon\mathscr U_k$. Уж тем более нет каких-то следствий посерьёзнее, в том числе для универсумов с $i+k+1$. Если что-то упускаю, поправляйте.

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