Double category construction from a functor to $\mathbf{Cat}$

80 Views Asked by At

Let $\mathbf{M}$ be a single-object category and $F$ a functor from $\mathbf{M}$ to $\mathbf{Cat}$. Let $X$ be image of the single object of $\mathbf{M}$ by $F$. It seems to me that the data of $F$ allows one to construct a double category $\mathbf{D}$ as follows:

  • The objects of $\mathbf{D}$ are those of $X$,
  • The horizontal morphisms of $\mathbf{D}$ are those of $X$
  • The vertical morphisms are the images of the morphisms of $\mathbf{M}$ by $F$, and thus compose like the morphisms of $\mathbf{M}$
  • Squares arise since the images of the morphisms of $\mathbf{M}$ are functors

Is this construction valid, and is it already known ?

My motivation comes from considering a category of open subsets and inclusion, and considering an additional group action on open subsets.