2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки




Начать новую тему Ответить на тему На страницу Пред.  1, 2
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение28.06.2015, 20:25 
Заслуженный участник


27/04/09
28128
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$ — как понимаю, этого уже достаточно для получения упомянутого вами парадокса?

 Профиль  
                  
 
 Re: Унивалентные основания математики. HoTT. Coq.
Сообщение27.07.2015, 16:34 


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

Я напишу текст как я понимаю некоторые моменты(в которых я сомневаюсь), и если в этом будет ошибка - надеюсь это заметят. Отмечу: "формеры" - калька с "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 для этих языков лучше развита? Наверняка это всё описывалось, только вот где?

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 17 ]  На страницу Пред.  1, 2

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group