Я философов не читал, я думал мы про Мартин-Лёфа

Да. Но, мне кажется (могу быть не прав), слово экстенсиональный у нас возникло в контексте разговора о том, как сравнивать стрелки в Hask.

Наверное, мы говорим всё же о funext?

Говорили про корреспонденции теорий типов и категорий в стиле Ламбека.
Насколько я понимаю, там обычно рассматривается выводимость терма какого-то типа в каком-то контексте как морфизм.
И равенство по построению этого терма как равенство морфизмов

Поэтому, чтобы контексты представлять категория должна быть как минимум моноидальная

Если нужны другие равенства с учётом редукций/семантики ими просто насыщают категорию

Тогда не очень понятно, почему curry f коммутирует, как нужно, с flip id. Мы показываем (во всех учебниках), что равенство выполняется, выполняя вычисление.

Т.е. в категорию добавляют конструкции/интродукции как морфизмы и ест. преобразования  и законы/переписывания как равенства между морфизмами на основе вашей теории.

Вот захотели и добавили бета редукцию как отдельное равенство/трансформацию, и сошлось как в учебнике

То есть, в Hask картинка такая: есть объекты - типы; есть морфизмы - термы; внутри каждого hom-множества вводятся эквивалентности (через beta-редукцию). Нужные свойства экспоненциала доказываются через применение цепочки бета-редукций, которые дают искомое равенство. Так?

А про это можно где-нибудь поподробнее почитать?

ну можно почитать просто про Lambek Correspondence или "Investigations into Linear Logic with Fixed-Point Operators Gavazzo"
там все равенства и правила можно сопоставить свойствам универсальных объектов либо построений

т.е. бета-редукция, как много раз говорили, просто выводится из сопряжения

т.е. для простой системы - наследницы STLC ничего особенного придумывать не нужно
а если какую-то модальную или исчисление секвенций, уже наверное, не так всё просто

А про Hask я так понимаю, не существует какого-то признанного её подмножества, подходящего для рассмотрения как непротиворечивая система. Каждый урезает по собственному вкусу

Меня больше интересует нечто вроде категории состояний КАМ и программ (или вычислений?), как морфизмов.

Вообще, кто-нибудь занимался такими категориями? Потому что состояния ВМ и программы пересчёта этих состояний, вроде, очевидно, категорию формируют.

Я понимаю в таком случае, как чисто операционно задать curry и eval. Но я не понимаю, какой смысл нужно вкладывать в морфизм. Чем f отличается от lambda f? На уровне машины f - цепочка инструкций. Но и lambda f - та же самая цепочка, но спецально помеченная маркером curry.

Можно ли говорить, что отличие в том, к каким объектам эти стрелки "прибиты"?

Возможно, чтобы стало хорошо, в качестве морфизмов следует рассматривать протоколы исполнения?

Теория категорий хорошо моделирует MLTT без равенств, где нормальная форма это стрелка, а объект это тип. Интенсиональное равенство можно, добавить, конечно, но это будут просто объекты такие, на структуру категории не влияющая. Веселье начинается когда берёшь OTT или HoTT (или Hask)