Categorified Container

Defined in gylterud2011-symmetric-containers-thesis.

$\mathrm{CCon}$ is defined as a strict 2-category:

• objects are $\_◃\_:(S:\mathrm{Cat})(P:S\Rightarrow \mathrm{Cat})\to \mathrm{Type}$
• homsets between $S\text{triangleleftP}$ and $T\text{triangleleftQ}$ are: $(F:S\Rightarrow T)\times (\sigma :Q\circ F\Rightarrow P)$
  Semantic brackets provide a strict 2-Functor $[[\_]]:\mathrm{CCon}\to {\mathrm{Cat}}^{\mathrm{Cat}}$, given by:
• Given $\mathcal{C}:\mathrm{Cat}$, Let $[[S\text{triangleleftP}]]\mathcal{C}$ be the category with:
  • objects $(s:S)\times (Ps\Rightarrow \mathcal{C})$.
  • morphisms between $s,\varphi$ and $t,\psi$ are:$(m:S[s,t])\times (\varphi \Rightarrow \psi \circ Pm)$
  • composition is given as,$(n,\beta )\circ (m,\alpha )=(n\circ m,\beta (Pm)\circ \alpha )$

Examples

If $S=1$ then, objects are just functors from $P\ast \Rightarrow \mathcal{C}$, essentially describing the class of diagrams in $\mathcal{C}$.
If $S$ is discrete and $Ps$ is discrete for all $s$, then $S\text{triangleleftP}$ is just a regular container.
If $S$ is a thin category given by preorder $\le$, and $P:S\to \mathrm{Cat}$ is contained in the subcategory $\mathrm{Poset}\subseteq \mathrm{Cat}$ of poset categories, then $[[S\text{triangleleftP}]]:\mathrm{Poset}\to \mathrm{Poset}$.
If $S$ is a groupoid and all $P:Ps\subseteq \mathrm{Grpd}$, then $[[S◃P]]$ is a groupoid.

Let $S:\mathrm{Cat}$. We can construct its categorical container $RS:\mathrm{CCon}$, setting $RS=S◃$

References

altenkirch2024-categorified-containers
gylterud2011-symmetric-containers-thesis