По просьбе os80 пишу ещё раз об унивалентности в ЖЖ

[akuklev]

(P.S. Кажется, я научился быстро писать. Весь нижеследующий пост написался за 15 минут за едой.)

Гомотопическая теория типов HoTT это такой фреймворк для деланья математики и одновременно язык программирования. Среди довольно обширного семейства таких систем* HoTT примечательна тем, что gets equality right.

Comments

[os80]

Прежде всего, громадное спасибо за отклик на чаяния масс в виде меня :-) У меня было нехорошее подозрение, что я (попытавшись читать HoTTBook) просто неправильно что-то переводил. Проблема, однако, более глубокая (я не понимаю кое-что на сущностном уровне), поэтому разрешите задать пару вопросов.
типы a = b теперь интерпретируются не как тип доказательств равенства a и b, а как тип сохраняющих структуру обратимых переходов от a к b
1. Что такое а и b? Может быть такое, что, например, а это число 3, а b - это число 6? Или, скажем, это больше похоже на "пусть a это множетство целых чисел, а b - множество чётных чисел"? Или даже на "пусть a это кольцо целых чисел, а b - кольцо чётных чисел"?
2. Что такое "обратимый переход"? Биекция/изоморфизм?
3. Что такое "3=6"? "Множество/класс" преобразований, переводящих 3 в 6? "Множество/класс" таких обратимых преобразований?
4. Что такое "Z = (Z/2Z)"? Умножение на двойку? Умножение на двойку в композиции со всеми перестановками?

[thedeemon]

a и b могут быть числами, функциями, типами, чем угодно, лишь бы одного типа.
Рассматривая их тип как пространство, а их самих как точки, значение "a=b" это путь в таком пространстве, а тип "a=b" это просто тип. В случае 3 и 6 такой тип будет ненаселен - не будет значений такого типа, нет пути из 3 в 6. Ибо натуральный числа - это дискретное пространство, там все пути идут из точки в саму себя, разные точки не соединяются.

В случае когда a и b это типы (вроде того же Z), уже интереснее. Там могут быть нетривиальные пути, и пространство этих путей эквивалентно пространству изоморфизмов между ними, что унивалентность и постулирует.

[os80]

>там все пути идут из точки в саму себя, разные точки не соединяются.
Почему? Что такое вообще "путь". akuklev перевёл path как "обратимый переход, сохраняющий структуру". Не знаю, насколько это верно, но хотя бы приблизительно понятно. Вы же используете понятие "пути" в каком-то нестандартном смысле и не вводите это понятие.

[akuklev]

Можно вместо "обратимый переход" попробовать термин "соответствие". Вот элемент множества неупорядоченных пар соответствует самому себе двумя способами: прямо так и с отзеркаливанием. Эти два способа совпадают между собой только если оба элемента пары равны.

[thedeemon]

Само слово это, как и "гомотопия", пришло из топологии. Подробное описание должно быть в упомянутой книжке по HoTT, а моя сумбурная попытка изложить это дело по-русски (которая появилась еще до выхода той книжки) есть тут.

[os80]

То есть "путь" это "identity type"?

[thedeemon]

Практически: identity type это пространство путей, а конкретные значения этого типа - конкретные пути.

[akuklev]

1. Чтобы повысить читабельность, следует не опускать индекс T у знака =. Т.е. для каждого типа T: Type есть также оператор _=T_: (T, T) -> Type. То есть a и b могут быть любыми сущностями общего типа T. Например, это могут быть натуральные числа Nat, тогда для каждых двух натуральных чисел a и b есть тип a =Nat b. Для 2 и 5 тип 2 =Nat 5 пуст. А вот тип 2 =Nat 2 населен одним и только одним элементом refl 2.

Но при этом типы это же тоже люди! Так что для типов A: Typen и B: Typen тоже существует тип A =Typen B: Typen - 1. И он содержит изоморфизмы между типами A и B. То есть, конструктивные взаимно-однозначные отображения между этими типами.
(Тут я в явном виде пишу, что типа "Type" на самом деле нет, а есть кумуллятивная иерархия вселенных Type n для всевозможных ординалов. А написание T: Type это просто abuse of notation, который убирает компилятор во время компиляции сам, подставляя нужный ординал в качестве индекса, либо ругаясь, если где-то случается неразрешимый замкнутый круг

[os80]

>Что такое "Z = (Z/2Z)" я могу только догадываться.
Да, фигню написал. Хотел написать "ℤ =Ring 2ℤ" (где pℤ - тот самый идеал, про который Вы написали, только он для любого p идеал, не только простого; а вот правильно ли использован индекс - не уверен).

[akuklev]

Да, я имел в виду, что для простого p это простой идеал. :-)

[akuklev]

Кроме того, это либо неопределённое выражение, либо пустой тип в зависимости от того, означает Ring унитальные кольца или возможнонеунитальные.

[os80]

Возможнонеунитальные. А почему пустой тип, ведь есть очевидный изоморфизм "умножение на двойку"?

[akuklev]

Потому что умножение на двойку это не изоморфизм. В исходном кольце есть элемент со свойством u*u = u, а во втором нет.

[sassa_nf]

a==b, например, может быть доказательством, что 0+x==x.

Но отсюда не очевидно, что y+(0+x)=y+x. Строим новый путь, который оказывается равен y+x==y+x.

Способов доказать этот факт может быть несколько: y+(0+x) == (y+0)+x & y+0==y => y + (0+x) == y+x - раз; более очевидное (0+x) == x & y+a==y+a => y + (0+x) == y+x - два; это разные пути. Их, стало быть, можно различать, говорить о равенстве путей, и т.д. вглубь.

Думаю, я полагаю правильно, что в то время, как в Агде эти преобразования нужно делать руками, в HoTT эти преобразования "автоматом" - как если бы здесь выбросить все эти path-*, оставить только суть, и оно будет компилироваться (а чтобы понять, что за проблема - вот возьмите, уберите их, и посмотрите, какие вещи Агде не очевидны). (За правильное использование терминологии там не ручаюсь)

[os80]

"Путь" - это доказательство? А почему тогда akuklev говорит про "обратимые преобразования" там, где в HoTTBook (я, правда, дальше начала 2 главы не прочитал) говорят о "путях"?

[akuklev]

Потому что в русском не устоялось терминологии и не разделяют witness и proof.
Напримеро witness существования какого-то такого x: T что выполняется P(x) это элемент w типа (x: T, P(x)), т.е. пара состоящая из этого самого x = fst w (он в явном виде предьявляется) и доказательства snd w, которое мы не можем вполне отделить от самого x, потому что у него тип P(x). Собственно элементы a = b это witnesses эквивалентности a и b. В конструктивном мире HoTT задать соответствие (естественно доказывая, что это соответствие), это и есть доказать равенство.

Вам надо привыкнуть к тому, что объекты несут в себе всякие свойства. Если мы пишем, что _+_: AssociativeOperation[T], то на практике мы конечно можем писать 2 + 3, но в недрах _+_ это пара из отображения Nat -> Nat -> Nat и доказательства, что это отображение ассоциативно.