Все вы знаете уже, что с августа 2017 года конструктивную интерпретация аксиомы унивалентности можно доказать не только на бумаге, но и используя тайпчекер cubicaltt. Но мало кто знает, что этот тайпчекер является устаревшим! Да да, начиная с марта 2018 года появилась новая конструктивная кубическая теория и ее тайпчекер yacctt, основанная не на примитивах композишина и склеек comp Glue glue glue, а на коершинах и гомогенных композициях coe, hcom, ghcom, gcom, com. Хотя и то и другое — операции Кана, последняя модель позволяет получить более компактные доказательства и более компактный тайпчекер. Основная мотивация такого пайвота в том, что на кубике не считается число Брунери n=2 в π_4(S^3) ≃ Z/nZ (канонический тест для гомотопического тайпчекера). Для этого оказывается 64ГБ памяти маловато! Правда на yacctt еще пока не написано, но уже видно, что основные унивалентные теоремы гораздо компактнее.
