Настроение:	pessimistic
Музыка:	Haus Arafna -- Rebels Have No King
Entry tags:	type theory, univalence

И ты, Брут, продался большевикам?
Новости из унивалентного мира:

Applications are invited for two postdocs and one PhD student to work on the recently funded EPSRC grant "Homotopy Type Theory: Programming and Verification" obtained by Professor Neil Ghani and Dr Conor McBride (University of Strathclyde), Dr Thorsten Altenkirch (University of Nottingham) and Dr Nicola Gambino (University of Leeds). One postdoc and will work on more theoretical aspects of the project in Nottingham, while the other postdoc will work on implementation issues in Strathclyde. Nevertheless, the reality is that we will be working as a team with frequent visits expected between ourselves and our collaborators.

Homotopy Type Theory (HoTT) is a revolutionary new approach to type theory where types are interpreted as spaces, terms as points and equalities as paths... Ну и так далее.

Короче говоря, МакБрайдушка теперь тоже с ними. Шаг, конечно, понятный -- у ребят проблемы с совместимостью унивалнтности и dependent pattern matching, а МакБрайд в последнем большой специалист. Однако, видимо, никакой другой теории типов кроме гомотопической в ближайшее время не будет. Есть конечно Эдвин Бреди, есть Роберт Эткей, есть ученик МакБрайда Пьер ``МакДаг'' Даган, есть наконец зеленая поросль аспиров, ``поднявшихся на здоровой закваске'', но думалось, что в бой против унивалентной чумы поведет их МакБрайд. Но нет, видимо вместо ожидавшегося второго Эпиграмма и прорывов в области refinement types нас ждут сотни страниц с диаграммами, симплициальными множествами и т.п. Ну может людям, который занимаются приложениями, вроде Ксавье Лероя надоест писать тактики в Ltac и они начнут заниматься, скажем, доказательством через рефлексию. Было бы здорово.

Есть еще Абель, Нилс и Ульф, но они вроде рубятся за sized types, а православный путь -- это memo-структуры или Bove-Capretta method.

Вот так, если у тебя есть премия Филдса, то ты можешь войти в любую область и наводить там свои порядки. Интересно посмотреть на становление гомотопической теории типов через призму приматологии науки. Ткачев слегка поехавший, but he's got a point. Всем сила и власть, пацаны!

Картинка для привлечения внимания: