Locally Graded Categories as Fibrations [efr-KR2F]
Locally Graded Categories as Fibrations [efr-KR2F]
There is also a para construction for enriched categories (say enriched in \mathcal {M}), where a parametrized morphism is defined in the evident curried way as a map P \to \mathcal {C}(A,B) in \mathcal {M}.
The natural generalization of enrichment and actions is the notion of locally \mathcal {M} graded category.
Locally graded categories were introduced by Wood in Reference [locally-graded-cats], under the name large \mathcal {M}-categories. The original motivation was to consider large presheaves on \mathcal {M} and use these to describe \mathcal {M}-enriched categories with possibly large hom-objects. We have not given much thought to size issues yet---our definition above should possibly be called "locally small locally graded categories". This is sufficient for us, since they capture all the \mathcal {M}-enriched categories and the locally small \mathcal {M}-actegories (as we will see in a bit,) which is what we're after.
The notion of locally graded categories turns out to be somewhat unhelpful in defining \mathsf {Para}(-), since the locally graded category corresponding to an category with an action is (a bicategorical version of) the \mathsf {Para}-construction applied to that case. Nevertheless, this does conceptually simplify certain things.
There is really nothing to show here. In the case of an actegory, conceptually we have the same idea---we want to define \mathcal {C}_M(X,Y) = \mathcal {C}(M \bullet X, Y)---but there is a bit more work to do to see that this comes together into a locally graded category. We begin with the following alternative description of locally graded categories:
From here, we will abuse terminology and freely refer to a category over B\mathcal {M} which is locally a discrete fibration as a locally graded category.
The idea now is that an action of \mathcal {M} can equivalently be described as a pseudofunctor B\mathcal {M} \to \mathsf {Cat}, and taking the 2-Grothendieck construction of this (in a suitable sense) will give us the locally graded category corresponding to this action.
By a 2-fibration we will always mean a 2-fibration in a weak sense, lying over a bicategory and classifying a pseudofunctor into bicategories (although our functors will always land in 1-categories). The correct notion of weak 2-fibration was first introduced by Buckley, Reference [buckley-2-fibrations]. (Recall that bifibration means a functor which is both a fibration and an opfibration, and so we can't use this word.)
As may be expected, the work of Buckley is extremely complicated, because he treats the full generality and thus must consider the tricategory of bicategories, and the class of trifunctors into it. We only care about actions on ordinary categories, and hence can restrict ourselves to the bicategory \mathsf {Cat}.
Recall that in the ordinary Grothendieck construction, there are actually two ways to turn a functor \mathcal {C}^\mathrm {op} \to \mathsf {Cat} into a category---we can either turn it into a fibration over \mathcal {C} or an opfibration over \mathcal {C}^\mathrm {op}. In the bicategorical case, there are two independent choices---we can be either contravariant or covariant both in the 1-cells and in the 2-cells. Somewhat annoyingly, the bicategorical structure usually put on \mathsf {Para} corresponds to being covariant in the 1-cells but contravariant in the 2-cells, forcing us to deal with this sort of "mixed-variance fibration" (\mathrm {co} \mathsf {Para}, consisting instead of morphisms X \to M \bullet Y, instead has the 2-cells going in the opposite direction, so there's no help there).
Hence, we have characterized both the actions of and the enrichments in \mathcal {M} as subcategories of the locally graded \mathcal {M}-categories.
Let us observe first that, as discussed above, the locally graded \mathcal {M}-category corresponding to an action or enrichment is really a bicategorical version of \mathsf {Para}
This will serve as a definition of the bicategory of parametrized maps. From this we can easily describe a double category of parametrized maps, which we will denote \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})
Note that a (pseudo) double category with singleton vertical category is equivalent to a monoidal category. Thus we can state:
Explicitly, for monoidal actions, we have:
We will see that the \mathsf {Para} construction preserves pseudo-limits, which will allow us build a triple category where one of the directions is parametrized maps, by applying the \mathsf {Para} construction levelwise to a double category internal to actions.