Замкнутые категории и теория доказательств

Основная цель работы – изложить некоторый перевод первоначальных понятий теории категорий на язык структурной теории доказательств и применить этот перевод для упрощения доказательств некоторых известных результатов [1] и для получения новых: теоремы когеррентности для канонических морфизмов в (немоноидальных, несимметрических) замкнутых категориях [2] и решения проблемы равенства канонических морфизмов; Намечено распространение этих результатов на моноидальные замкнутые, симметрические замкнутые и моноидальные симметрические замкнутые категории. Разрешающий алгорифм получается с помощью корректного и полного перевода канонических морфизмов в некоторое расширение $\lambda$-языка, содержащее средства для специального учета “лишних” посылок импликаций (правило утончения). Расширения $\lambda$-языка, рассматривавшиеся в литературе до сих пор,таких средств не содержали. Библ. 23 назв.