Formal aspects of Gray's tensor product of 2-categories
Alexandru E. Stanculescu
TL;DR
This paper formalizes Gray's tensor product of 2-categories, focusing on the construction of right internal and internal homs within its two monoidal structures.
Contribution
It provides a rigorous formalization of Gray's tensor product and the associated internal hom constructions for small 2-categories.
Findings
Formalization of Gray's tensor product
Construction of right internal homs
Construction of internal homs
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsHomotopy and Cohomology in Algebraic Topology · Algebraic structures and combinatorial models · Advanced Topics in Algebra