Has there been any work done on internal categories inside internal categories?

I'm familiar with $n$-fold categories, but I don't want an internal category inside the category of internal categories in a category with pullbacks, I want an internal category inside *another internal category*. I can think of two approaches, but I can only work out the details fully on one of them.

The first approach externalizes an internal category, then looks at an internal category inside the externalization of this internal category. In detail:

Let $\mathcal{B}$ be a category with pullbacks and a terminal object ${\bf 1}$, hence all limits, and let ${\sf C}$ be an internal category in $\mathcal{B}$ with ${\sf Fam(C)}\to\mathcal{B}$ the internal family fibration of ${\sf C}$. Consider the fiber ${\sf Fam(C)}_{\bf 1}$ of this fibration over the terminal object in $\mathcal{B}$; we view this as an 'externalized version' of ${\sf C}$, justified by the fact that in the family fibration ${\sf Fam}(\mathcal{C})\to{\bf Set}$ of an arbitrary category $\mathcal{C}$ we have $\mathcal{C}\cong{\sf Fam}(\mathcal{C})_1$. Assume that ${\sf Fam(C)}_{\bf 1}$ has pullbacks. A ${\bf reclusive\ category}$ is an internal category inside ${\sf Fam(C)}_{\bf 1}$ for some internal category ${\sf C}$ inside a category with limits.

We can justify this approach by 'externalizing one step' and setting $\mathcal{B}={\bf Set}$, observing that a reclusive category in the category of sets is an internal category inside a category with pullbacks.

The second approach attempts to directly define an internal category inside another one without first externalizing, but I run into some issues expressing internal pullbacks; we could express commuting diagrams internally, and I know Jacob's book covers internal products and equalizers so we should be able to reconstruct internal pullbacks, but I haven't worked out the details yet. So far I have the following, using arrows out of the terminal object to select the objects and arrows we need inside the internal category:

Let $\mathcal{C}$ be a category with limits, and let ${\sf C}$ be an internal category in $\mathcal{C}$. We define a ${\bf reclusive\ category}$ $\mathscr{C}$ in ${\sf C}$ to consist of the following data:

- An arrow $$ {\bf Ob}_\mathscr{C}:{\bf 1}\to{\sf Ob_C}. $$
- An arrow $$ {\bf Hom}_\mathscr{C}:{\bf 1}\to{\sf Ob_C}. $$
- Two arrows $$ {\sf dom}^\mathscr{C},{\sf cod}^\mathscr{C}:{\bf 1}\to{\sf Hom_C} $$ such that the following diagrams commute

- An arrow $$ 1^\mathscr{C}:{\bf 1}\to{\sf Hom_C} $$ such that the following diagrams commute

- An arrow $$ \circ^\mathscr{C}:{\bf 1}\to{\sf Hom_C} $$ ...

This is where I have to trail off with this approach, since we would need to form an internal pullback of the selected internal object of arrows with itself over the internal object of objects, but I think this approach should be justified by the fact that if we externalize one step again by setting $\mathcal{C}={\bf Set}$ we get the same result as above (although we may need to tweak the above definition to assert that the internal category $\mathcal{C}$ has internal pullbacks). Any references or assistance are appreciated.

globalobject of the internal category, i.e. a morphism $1 \to \operatorname{ob} \mathcal{C}$, or should it be a generalised object with global support, i.e. a morphism $T \to \operatorname{ob} \mathcal{C}$ such that $T \to 1$ is a (covering) epimorphism? (Of course we also impose conditions on the object of morphisms but I omit them here.) $\endgroup$ – Zhen Lin Apr 3 at 8:39reclusivefour times, it can't be a typo, so why did you choose that name? $\endgroup$ – Paul Taylor Apr 4 at 20:231more comment