The question: I wonder whether the following definition, or something similar, has appeared somewhere (see below for motivations). Any reference or pointer is welcome!
(In what follows, I denote horizontal composition by $\cdot$ and vertical composition by $\ast$).
Let $\mathcal D$ be a (strict) double category, let $f:a\to b$ be a horizontal morphism and $p:b'\to b$ a vertical morphism. Let us define a cartesian lifting of $f$ with respect to $p$ to be a cell $\alpha$
such that, for every cell $\alpha'$ whose vertical target is $p$ and whose horizontal target is $f\cdot g$ for some $g$, there exist unique cells
such that $\alpha'=(\alpha\ast\delta)\cdot\gamma$. Pictorially:
We may call "fibrational" a double category in which cartesian liftings always exist. This seems to be unrelated to the notion of fibrant double category or framed bicategory.
The name "fibrational" is justified by the fact that a functor $F:\mathcal A\to\mathcal B$ induces a double category $\mathcal D(F)$ on the disjoint union of $\mathcal A$ and $\mathcal B$ (vertical morphisms are relations $F(a)=b$ and cells are relations $F(f)=g$; vertical composition is degenerate) such that $\mathcal D(F)$ is "fibrational" iff $F$ is a fibration (the cell $\delta$ is always the identity because of the degeneracy of vertical composition).
My motivations: I am studying term rewriting from a categorical perspective: terms are objects, rewriting paths are arrows. In particular, I am interested in formulating infinitary term calculi as ideal completions of finitary calculi. It is very natural to equip both terms and rewrites with a partial order relation yielding a posetal double category, i.e., a category internal to $\mathbf{Pos}$, the category of posets and monotonic functions. These may be seen as double categories in which vertical arrows are order relations between objects and cells are order relations between horizontal arrows (whose source and target are related).
Let $\mathbf{Dcpo}$ be the category of directed-complete partial orders and Scott-continuous functions. It is well known that the forgetful functor $\mathbf{Dcpo}\to\mathbf{Pos}$ has a left adjoint, called ideal completion. By contrast, it is not hard to see that the forgetful functor $\mathbf{Cat}(\mathbf{Dcpo})\to\mathbf{Cat}(\mathbf{Pos})$ does not have a left adjoint, so a posetal double category does not admit an "ideal completion" in general. However, one may show that if a posetal double category $\mathcal D$ is such that $\mathcal D^{\mathrm{tcoop}}$ is "fibrational", then its ideal completion may be defined ($\mathcal D^{\mathrm{tcoop}}$ is the double category obtained from $\mathcal D$ by swapping horizontal and vertical arrows and then reversing their direction). In other words, the forgetful functor has a left adjoint once we restrict to the subcategories of $\mathbf{Cat}(\mathbf{Dcpo})$ and $\mathbf{Cat}(\mathbf{Pos})$ in which objects are "tcoop-fibrational". Term calculi, with their order, turn out to be "tcoop-fibrational", so all the constructions I am interested in fit within this framework.
Since my motivations are quite peculiar, I am unsure about the general mathematical significance of the above definition, and I am not surprised I can't find it anywhere. Still, I thought it would be worth asking.
