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◁P$ and $T◁Q$ are: $\Sigma F:S\Rightarrow T.\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◁P]]\mathcal{C}$ be the category with:
  • objects $\Sigma s:S.Ps\Rightarrow \mathcal{C}$.
  • morphisms between $s,\varphi$ and $t,\psi$ are:$\Sigma m:S[s,t].\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◁P$ 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◁P]]:\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