String diagrams for 4-categories and fibrations of mapping 4-groupoids (Q6634614)

This paper introduces a string diagram calculus for strict 4-categories, using it to establish that given an inclusion of 4-categorical presentations \(\mathcal{P}\hookrightarrow\mathcal{Q}\) with \(\mathcal{Q}\) obtained from \(\mathcal{P}\) by the addition of a finite number of generating cells, the induced restriction functor on mapping spaces to a fixed target strict 4-category is a fibration of strict 4-groupoids.\N\NThe main result is the following theorem.\N\NTheorem. Let \(\mathcal{C}\) be a strict 4-category, \(\mathcal{P}\) a presentation and \(\mathcal{Q}\) another presentation, obtained by adding a finite number of cells in \(\mathcal{P}\). Then the restriction map\N\[\N\mathrm{Map}\left( \mathcal{Q},\mathcal{C}\right) \rightarrow\mathrm{Map} \left( \mathcal{P},\mathcal{C}\right)\N\]\Nis a fibration of strict 4-groupoids.\N\NThe papers [\textit{M. Araújo}, Compositionality 4, No. 2, 30 p. (2022; Zbl 1509.18024); ``Coherence for adjunctions in a $4$-category'', Preprint, \url{arXiv:2207.02935}] use the results of this paper to establish coherence results for adjunctions in strict 3- and 4-categories, which can then be used to give a simplified proof of the result in [\url{https://ora.ox.ac.uk/objects/uuid:a4b8f8de-a8e3-48c3-a742-82316a7bd8eb}] on coherence for 3-dualizable objects in strict symmetric monoidal 3-categories.