# Cartesian liftings in double categories

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.

• I haven't thought through this carefully, but here's a superficial analogy: another type of object in a double category with a universal property which mixes the vertical and horizontal parts in an interesting way, is a pointwise Kan extension, as here. Perhaps the notion is related (and perhaps with horizontals and verticals flipped). – Tim Campion Sep 21 '17 at 16:11