Is there way to formalize the idea that a category can be "cocomplete from the inside"?

Question

Let $\mathrm{KSet}$ denote the category of all countable sets, including the finite ones. Then $\mathrm{KSet}$ is finitely complete. Furthermore, $\mathrm{KSet}$ admits all countable colimits, or, less formally, it is "cocomplete from the inside." Is there way to formalize this idea (that a category can be "cocomplete from the inside") using structuralist language?

Answer 1

Let $\mathcal{S}$ be a category with pullbacks. An $\mathcal{S}$-indexed category $\mathbb{C}$ is a pseudofunctor $\mathcal{S}^\mathrm{op} \to \mathfrak{CAT}$, and $\mathbb{C}$ is said to be $\mathcal{S}$-cocomplete if the following conditions are satisfied:

• For each object $X$ in $\mathcal{S}$, the category $\mathcal{C}^X = \mathbb{C} (X)$ has finite colimits.
• For each morphism $f : X \to Y$ in $\mathcal{S}$, the functor $f^* : \mathcal{C}^Y \to \mathcal{C}^X$ preserves finite colimits.
• For each morphism $f : X \to Y$ in $\mathcal{S}$, the functor $f^* : \mathcal{C}^Y \to \mathcal{C}^X$ has a left adjoint, say $\Sigma_f : \mathcal{C}^X \to \mathcal{C}^Y$.
• The functors $\Sigma_f : \mathcal{C}^X \to \mathcal{C}^Y$ satisfy the Beck–Chevalley condition with respect to pullback squares in $\mathcal{S}$.

Observe that there is an obvious $\mathcal{S}$-indexed category $\mathbb{S}$ defined by $X \mapsto \mathcal{S}_{/ X}$. $\mathbb{S}$ automatically satisfies the last two conditions, and $\mathbb{S}$ is $\mathcal{S}$-cocomplete precisely when it is an extensive category with (pullbacks and) pullback-stable coequalisers. In particular, the category of countable sets is such a category.

We can dualise the above to obtain the notion of an $\mathcal{S}$-complete $\mathcal{S}$-indexed category. $\mathbb{S}$ is $\mathcal{S}$-complete if and only if $\mathcal{S}$ is a locally cartesian closed category; and if $\mathcal{S}$ also has finite colimits, then it is also $\mathcal{S}$-cocomplete.