Ну я в итоге несколько часов назад решил отделаться
, тем более что в итоге получилась ошибка в формулировке исчисления, которую я не знаю как исправить, так что ничего больше писать пока не надо. А вообще я почти три раза в исходном посте изобразил, что это должно быть — распилим мысленно
пополам и получим нечто вроде
первым куском, который и интересует (потому что второй-то везде есть).
Предполагалось использовать их в термах типов навроде такого:
, но я честно не понимаю, кому и чем такой пример может что-то пояснить. Главное чтобы два куска воспринимались как части одной распиленной стрелки, потому что они предполагались функционировать как половины функции, одна указывать принятие аргумента и другая выдачу результата.