(no subject)

Тут вчера Тьери Коканд разразился новой публикацией: Variation on cubical sets.

Вроде как всё круто, наконец-то модель гомотопической теории типов, в которой equality elimination rule верно дефиниционально. Может кто-нибудь хочет перевести это на земной язык и показать как всё это работает на пальцах? Я сходу не врубаюсь совершенно, а время на то чтобы разобрать хорошо если к новому году найду.