По просьбе os80 пишу ещё раз об унивалентности в ЖЖ

(P.S. Кажется, я научился быстро писать. Весь нижеследующий пост написался за 15 минут за едой.)

Гомотопическая теория типов HoTT это такой фреймворк для деланья математики и одновременно язык программирования. Среди довольно обширного семейства таких систем* HoTT примечательна тем, что gets equality right. ( Read more... )