The initial algebra of a polynomial functor over a slice category models W-types/induction.
I wanted to figure out dependent induction over some complicated categorical constructions.
I thought "W-types" in Cat might help. Cat has pullbacks so this should be possible in theory. But this turned out to be way too complicated for me to understand even though in theory "W-Cat" could be carved out.
I thought that it might be possible to figure out a subobject in an arrow category. But this seems like an ambiguous concept to me. More broadly this sort of concept should work for any sort of higher geometry right?
I can think of a few ideas.
A bundle of a presheaf.
$$[\Delta^{\mathrm{op}}, C]/c$$
A presheaf of a bundle.
$$[\Delta^{\mathrm{op}}, C/c]$$
But also the presheaf over a simplicial set is
$$[C^{\mathrm{op}}, [\Delta^{\mathrm{op}}, \mathrm{Set}]]$$
But this curries.
This suggests to me I might really want something like
$$(C \times \Delta) / \langle c , n \rangle$$
Which I guess you could think of a span between $C$ and $\Delta$