Естественное преобразование ловит ошибку, которую не видит больше ничто в дереве

Первый практический ответ на вопрос «зачем нам теоркат».

До этого все проверки категорий гоняли на сетках синтетических значений — полезно, но абстрактно. Здесь другое.

Пример — единицы измерения (examples/cat/natural-square.flang). Два взгляда на одни данные: «то же в рублях» и «то же в копейках», плюс перевод между ними. Забудьте про единицы ровно один раз — поставьте в наценку 100 вместо 1000 — и файл не соберётся, с предъявленным контрпримером.

И главное:

Ни одна другая проверка в дереве этой ошибки не видит. Функция остаётся тотальной. Типы сходятся. Свой пример подгоняется. Тесты зелёные.

Вот класс, который теоркат закрывает: согласованность между слоями. Именно такие ошибки живут в проде годами.

Честная оговорка про ассоциативность. Она заработала, но краснеть на честной программе пока не может: композиция в flang не пишется автором, она разворачивается в применение функций, а применение ассоциативно по построению. Чтобы проверка стала настоящей, композиции нужно своё объявленное равенство. Записано как задуманное, а не выдано за сделанное.

Ветка work/morphism-equality, вершина 4fd9cd6. Изъятие в 13 местах, каждое краснеет поимённо.

Связано: category-theory-transports-truth, a-removal-must-turn-a-test-red