Узкоспециальное

Я понял, чем мне не нравится деятельность вокруг HoTT, помимо общей странности затеи (испортить теорию типов гомотопиями). Это уже совсем не похоже на фундаментальную науку! Идёт некоторая инженерная деятельность, вроде "создания языка Go" (но создатели Go и не претендуют на большее). К Воеводскому как раз претензий нет, он доказывал теоремы о гомотопиях и проверял их пруфчекером, а вот вся орава, что за ним бросилась, или слегка одурела, или преследует коммерческие цели, одно другому тоже не мешает.

Немного кошачей музыки

Это мне приспичило найти одну Галину песню, которой я забыл название и где искать тоже забыл. Пришлось прослушать несколько гигабайт Галиного творчества, вот самые яркие находки.