![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Семинарчик?
Sep. 13th, 2015 01:17 amНу что, Кокан опубликовал ещё раз обновлённую версию вычинтерпретации HoTT: http://www.cse.chalmers.se/~coquand/face.pdf
(Теперь в приложении рассказывается про то, как там унивалентно построить стандартную предикативную иерархию вселенных вместе с операцией композиции идентификаций на ней.)
Никто не хочет сделать по этой штучке распределённый семинар? Т.е. попилить эту штуку на пяток-десяток частей, каждый участник берёт себе часть, подробно разбирает её и рассказывает о ней. Можно вживую, можно по скайпу, можно под запись, чтобы интересующийся народ послушал.
В качестве пререквизитов хотелось бы ограничиться HoTT Book, знанием теорката на уровне CftWM МакЛейна + какого-нибудь вводного текста про симплициальные множества, комплексы Кана и квазикатегории, т.е. возможно потребуются дополнительные доклады про какие-то неэлементарные аспекты теории кубических множеств и т.п.
(Теперь в приложении рассказывается про то, как там унивалентно построить стандартную предикативную иерархию вселенных вместе с операцией композиции идентификаций на ней.)
Никто не хочет сделать по этой штучке распределённый семинар? Т.е. попилить эту штуку на пяток-десяток частей, каждый участник берёт себе часть, подробно разбирает её и рассказывает о ней. Можно вживую, можно по скайпу, можно под запись, чтобы интересующийся народ послушал.
В качестве пререквизитов хотелось бы ограничиться HoTT Book, знанием теорката на уровне CftWM МакЛейна + какого-нибудь вводного текста про симплициальные множества, комплексы Кана и квазикатегории, т.е. возможно потребуются дополнительные доклады про какие-то неэлементарные аспекты теории кубических множеств и т.п.
