Formal aspects of Gray's tensor product of 2-categories
arXiv:1003.1994
Abstract
The category of small 2-categories has two monoidal structures due to John Gray: one biclosed and one closed. We propose a formalisation of the construction of the right internal and internal homs of these monoidal structures.
Title has been changed, major revisions and corrections, accepted in Appl. Categ. Str