Теорема когеррентности для канонических морфизмов в декартово замкнутых категориях

В работе доказана теорема когеррентности в теоретико-доказательственной формулировке: все выводы уравновешенной секвенции эквивалентны. (Секвенция называется уравновешенной, если каждая переменная входит в нее не более двух раз). Канонические морфизмы в декартово замкнутой категории – это морфизмы, которые можно получить из явно упоминаемых в определении декартово замкнутой категории (т.е. левой и правой проекций $l\colon A\times B\to A$ и $r\colon A\times B\to B$, $\varepsilon\colon A\times\hom(A,B)\to B$ и т.д.) с помощью композиции функторов $\times$, $\hom$ и операции $+$.
Пусть объекты $A$ и $B$ строятся из объектов $C_1,\dots,C_n$ при помощи функторов $\times$ и $\hom$. Тогда, вообще говоря, не все канонические морфизмы из $A$ в $B$ будут равны. Например, если $A$ есть $C_1\times C_1$, а $B$ есть $C_1$, то левая и правая проекции – различные морфизмы. Теорема когеррентности утверждает, что если не делать лишних отождествлений объектов, то все канонические морфизмы из $A$ в $B$ будут равны, т.е. все диаграммы канонических морфизмов с началом в $A$ и концом в $B$ будут коммутировать.
Известен перевод некоторых понятий теории категорий на язык теории доказательств, при котором объектам соответствуют формулы, а функторы $\times$ и $\hom$ интерпретируются как связки $\&$ и $\supset$. При этом переводе каноническим морфизмам из $A$ в $B$ соответствуют выводы в ($\&$, $\supset$) – фрагменте интуиционистского исчисления высказываний секвенции $A\to B$. Морфизмы равны тогда и только тогда, когда соответствующие им выводы эквивалентны, т.е. совпадают некоторые их нормальные формы или, что то же, эквивалентны их дедуктивные термы. Доказанная в работе теорема равносильна теореме когеррентности в алгебраической формулировке. Приводятся два доказательства этой теоремы, независимо полученные авторами, в одном из которых рассматриваются натуральные выводы и используется аппарат дедуктивных термов, а другое опирается на редукцию глубины формул с сохранением эквивалентности выводов, специализацию формы вывода в генценовских $L$-системах и анализ зацеплений в секвенциях. Библ. – 9 назв.