What is a correct notion of an internal pseudofunctor?

Question

Let $C$ be a category internal to a category $K$. It is well known (for example see Proposition 2.4 in the paper Higher Dimensional Algebra VI: Lie 2-Algebra by Baez and Crans https://digitalcommons.lmu.edu/cgi/viewcontent.cgi?article=1068&context=math_fac) that there is a strict 2-category $K$Cat consisting of categories in $K$ as objects, functors in $K$ as 1-morphisms and natural transformations in $K$ as 2-morphisms.

My question is the following:

Is there any existing notion of a pseudofunctor $F: C^{\rm{op}} \rightarrow K\rm{Cat}$? As of now, I could not find much about such notions.

If I define such a notion naively as

. every $x \in \rm{Ob}(C)$ is mapped to a category $F(x)$ in $K$,

. every $\gamma :x \rightarrow y \in \rm{Mor}(C)$ is mapped to a functor $\gamma^{*} : F(y) \rightarrow F(x)$ in $K$,

. such that functoriality hold upto certain choices of natural isomorphisms in $K$,

. such that "these choices of natural isomorphisms" satisfy the standard coherence properties similar to the usual category valued pseudofunctors,

then what are the problems we may face?

Thanks in advance!

Answer 1

Let $\mathcal{C}$ be a category with pullbacks, with ${\sf C}$ an internal category in $\mathcal{C}$. We define a category $${\sf Ext( C})$$ called the externalization of ${\sf C}$ as follows:

1. The objects of ${\sf Ext(C)}$ are generalized elements of ${\sf Ob_C}$, that is arrows $x:X\to{\sf Ob_C}\in{\bf Hom}_\mathcal{C}$.
2. The arrows $f:x\to y$ of ${\sf Ext(C})$ are ordered pairs $(u,f)$, where $u:dom(x)\to dom(y)\in{\bf Hom}_\mathcal{C}$ and $f:dom(x)\to{\sf Hom_C}$ is a generalized element of ${\sf Hom_C}$, which commute appropriately with ${\sf dom}$, ${\sf cod}$, $x$ and $y$. That is, we have $${\sf dom}\circ f=x,$$ $${\sf cod}\circ f=y\circ u.$$
3. Identities on objects are given by the identity on their domains in the first coordinate and the postcomposition of that object with the internal identity selecting arrow for ${\sf C}$ in the second coordinate. That is, $$1_x=(1_{dom(x)},1_{\sf C}\circ x).$$
4. Composition is given pointwise in the first coordinate and by induced pullback arrows postcomposed with internal composition in the second coordinate. That is, for arrows $(u,f):y\to z$ and $(v,g):x\to y$ we define $$(u,f)\circ(v,g)=\big(u\circ v,\circ_{\sf C}\circ\langle f\circ v,g\rangle\big)$$ where $\langle f\circ v,g\rangle:dom(g)\to{\sf Hom_C\times_{_{Ob_C}}Hom_C}$ is a uniquely induced pullback arrow.

We can then consider a regular indexed category $$\Phi:{\sf Ext(C)}^{op}\to\mathcal{\sf Cat}(\mathcal{C})$$ where ${\sf Cat} (\mathcal{C})$ is the $2$-category of internal categories in $\mathcal{C}$, and this is naively the shortest answer to 'what is the correct notion of an internal indexed category'.

Note that we can externalize internal functors and natural transformations in similar fashion, yielding a $2$-functor $${\sf Ext}:{\sf Cat}(\mathcal{C})\to\mathfrak{Cat}$$ which is faithful, but not generally full -- the above suggestion thusly isn't the right answer to 'what is the correct notion of an internal indexed category', in general.

We can obtain a full embedding by fixing the object we're externalizing from instead of using arbitrary objects from the base category, but we then lose faithfulness unless the object we choose is a separator. Externalizing from a separator $S$ yields a full and faithful embedding $${\sf Ext}_S:{\sf Cat}(\mathcal{C})\hookrightarrow\mathfrak{Cat}$$ allowing us to really work with internal data as though it were regular external data, so the answer to 'what is the correct notion of an internal indexed category' in a category admitting a separator $S$ would be a regular indexed category $$\Phi:{\sf Ext}_S({\sf C})^{op}\to{\sf Cat(}\mathcal{C}).$$

All of this is really an internal version of the family fibration for a category and is clearer through the lens of fibered category theory; for more details, see p. 246-264 of these notes.