The HoTT Book

[nivanych]

http://homotopytypetheory.org/book/
http://homotopytypetheory.org/2013/06/20/the-hott-book/
http://golem.ph.utexas.edu/category/2013/06/the_hott_book.html

Comments

[kurilka]

в жуйке мне никто не ответил, поэтому спрошу ещё и тебя - а простым смертным стоит грызть сей гранит, или оно сильно для математиков?

[nivanych]

Первая мысль - стоит, конечно, штуки интересные.
В зависимости от своих знаний - что-нибудь, да поймёшь хорошего ;-)
А вообще, я ещё книжку не смотрел ;-)
Ннуу, (∞,1)-категорная сущность этих вещей мне понятна, подробно разбираться буду потом.
Завтра, как минимум, просмотрю книжку.
И что-то сюда тебе напишу.

[kurilka]

заранее спасибо

[nivanych]

Посмотрел. Неплохо, чисто написано.
Я бы даже сказал, что по бОльшей части, книжка философская ;-)
Материалы похожи на переработанные статьи с ncatlab.

[kurilka]

т.е. стоит пролистать чтоб проникнуться этими "унивалентностями"?

[nivanych]

Я не думаю, что будет сложно читать.

[kurilka]

ещё раз спасиб

[nivanych]

Посмотрел подробнее.
Ну так это ж почти учебник.
Причём, написанный довольно толково.
В любом случае, есличо непонятно, то можно же и спросить ;-)
Где спрашивать...
Видимо, в ru_deptypes или ru_ declarative будет уместнее всего. Может быть, ru_lambda.
Возможно, что и в category_theory. Гарантирую, что модератор против не будет ;-)
Только ответы, возможно, будут специфические.

[kurilka]

ок, поднимем в списке к прочтению поближе

[nivanych]

Понимание первой главы (я пока только парочку прочитал) вполне может упростить освоение Agda/CoQ.