Sep. 13th, 2015

akuklev: (ДР Цертуса 2011)
Ну что, Кокан опубликовал ещё раз обновлённую версию вычинтерпретации HoTT: http://www.cse.chalmers.se/~coquand/face.pdf
(Теперь в приложении рассказывается про то, как там унивалентно построить стандартную предикативную иерархию вселенных вместе с операцией композиции идентификаций на ней.)

Никто не хочет сделать по этой штучке распределённый семинар? Т.е. попилить эту штуку на пяток-десяток частей, каждый участник берёт себе часть, подробно разбирает её и рассказывает о ней. Можно вживую, можно по скайпу, можно под запись, чтобы интересующийся народ послушал.


В качестве пререквизитов хотелось бы ограничиться HoTT Book, знанием теорката на уровне CftWM МакЛейна + какого-нибудь вводного текста про симплициальные множества, комплексы Кана и квазикатегории, т.е. возможно потребуются дополнительные доклады про какие-то неэлементарные аспекты теории кубических множеств и т.п.

December 2016

S M T W T F S
    123
456789 10
11121314151617
18192021222324
25262728293031

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Aug. 30th, 2025 04:29 am
Powered by Dreamwidth Studios