The Gray tensor product via factorisation

TL;DR

This paper presents a new approach to constructing the Gray tensor product of 2-categories using universal properties and factorisation systems, simplifying previous methods and reinforcing its symmetric monoidal structure.

Contribution

It introduces a universal property-based factorisation method to define the Gray tensor product without explicit presentations, providing a new proof of its symmetric monoidal structure.

Findings

Gray tensor product can be obtained via factorisation without explicit presentation

The method uses Lawvere 2-theories and factorisation systems

Confirms Gray tensor product as part of a symmetric monoidal structure

Abstract

We discuss the folklore construction of the Gray tensor product of 2-categories as obtained by factoring the map from the funny tensor product to the cartesian product. We show that this factorisation can be obtained without using a concrete presentation of the Gray tensor product, but merely its defining universal property, and use it to give another proof that the Gray tensor product forms part of a symmetric monoidal structure. The main technical tool is a method of producing new algebra structures over Lawvere 2-theories from old ones via a factorisation system.