Internal $2$-categories

Question

Has the notion of an internal $2$-category been studied, or more generally an internal $n$-category? Do we have any examples of naturally occurring internal $2$-categories/$n$-categories?

The motivation here is understanding internalization at higher levels.

In particular, it seems the 'nuts and bolts' set theoretical definitions of higher $n$-categories as a class of objects, a class of $1$-cells, a class of $2$-cells, ..., a class of $n$-cells, together with functions between them for domains, codomains, and identities, and functions out of pullbacks for compositions (see below for an example), is more naturally internalized at higher levels than the 'high-tech' definitions relying on component $n-1$ categories for each pair of objects together with $n-1$ functors for composition, $n-1$ natural transformations for associative coherence, $n-1$ modifications for coherence of associative coherence, $\dots$.

This seems counterintuitive (even ironic) in light of the goal of internal category theory -- internalization is supposed to allow us to eschew any use of sets in our categorical reasoning, but we have to use a very set theoretical definition of higher categories in order to correctly internalize them? Perhaps I'm just not seeing a simple internalization of the latter definition.

To make the question more precise, here's one possible internalization of the 'nuts and bolts' definition of a bicategory on the nlab:

---

Let $\mathfrak{C}$ be a $2$-category with $1$-cell pullbacks. An internal $2$-category $\mathrm{C}$ in $\mathfrak{C}$ consists of

1. An object of objects ${\bf Ob}_\mathrm{C}\in{\bf Ob}_\mathfrak{C}$.
2. An object of $1$-cells ${\bf 1-Hom}_\mathrm{C}\in{\bf Ob}_\mathfrak{C}$.
3. An object of $2$-cells ${\bf 2-Hom}_\mathrm{C}\in{\bf Ob}_\mathfrak{C}$.
4. $1$-cells as below for domains, codomains and identities:
5. $1$-cells as below for vertical and horizontal composition: where we pull back ${\bf 2-Hom}_\mathrm{C}$ over ${\bf 1-Hom}_\mathrm{C}$ using ${\sf dom}$ and ${\sf cod}$ for vertical composition, and over ${\bf Ob}_\mathrm{C}$ using ${\sf dom\circ dom}$ and ${\sf cod\circ cod}$ for horizontal composition.
6. A $2$-cell $\gamma$ as below for associative coherence of composition:
7. $2$-cells $\iota_\ell$ and $\iota_r$ as below for left and right unital coherence:

With all the above data satisfying appropriate coherence diagrams (in the spirit of bicategories), this definition seems to shake out correctly -- realized in the discrete $2$-category ${\bf Set}$ this yields a strict $2$-category, since all $2$-cells will be identities. Realizing it in the $2$-category of categories yields something else, a 'triple category' of sorts, but perhaps this discrepancy has to do with the fact that we've internalized a set-theoretical definition of $2$-categories rather than a $1$-categorical definition.

Has this idea been explored, or is it trivialized by some higher notion of internal categories already in the literature?

Answer 1

Bicategories internal to 2-categories with pullbacks are defined in §3 of Douglas–Henriques's Internal bicategories. They have two motivating examples described in §1: a bicategory $\mathrm{Bord}_0^2$ of bordisms internal to the 2-category $\mathrm{CAT}$; and a bicategory of conformal nets internal to the 2-category $\mathrm{SYMMONCAT}$.