Geodesic
Equality of maps and coherence theorem for biclosed categories
Zapiski Nauchnykh Seminarov POMI, Theoretical application of methods of mathematical logic. Part III, Tome 105 (1981), pp. 3-9 
A. A. Babaev. Equality of maps and coherence theorem for biclosed categories. Zapiski Nauchnykh Seminarov POMI, Theoretical application of methods of mathematical logic. Part III, Tome 105 (1981), pp. 3-9. http://geodesic.mathdoc.fr/item/ZNSL_1981_105_a1/
@article{ZNSL_1981_105_a1,
     author = {A. A. Babaev},
     title = {Equality of maps and coherence theorem for biclosed categories},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {3--9},
     year = {1981},
     volume = {105},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_1981_105_a1/}
}
TY  - JOUR
AU  - A. A. Babaev
TI  - Equality of maps and coherence theorem for biclosed categories
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 1981
SP  - 3
EP  - 9
VL  - 105
UR  - http://geodesic.mathdoc.fr/item/ZNSL_1981_105_a1/
LA  - ru
ID  - ZNSL_1981_105_a1
ER  - 
%0 Journal Article
%A A. A. Babaev
%T Equality of maps and coherence theorem for biclosed categories
%J Zapiski Nauchnykh Seminarov POMI
%D 1981
%P 3-9
%V 105
%U http://geodesic.mathdoc.fr/item/ZNSL_1981_105_a1/
%G ru
%F ZNSL_1981_105_a1

Voir la notice du chapitre de livre provenant de la source Math-Net.Ru

The problems in question are reduced here to ones for closed categories solved in [2,3]. First a natural deduction system is constructed and a term is assigned to any derivation. Equivalence relation ($\underset{BC}\equiv$) is defined for terms. Next a term is assigned to every canonical map and it is proved that two canonical maps are equal iff corresponding terms are equivalent. Finally, using the results from [2,3] we present decision algorithm for ($\underset{BC}\equiv$) and prove coherence theorem for canonical maps in ВС categories.