Profunctorial Grothendieck Construction?

Question

I've been taking the ideas expressed in "Functors are Type Refinement Systems" seriously lately and it's lead me to a form of the Grothendieck construction I've never seen before.

The idea in that paper is to think of a programming language $T$ as a category of terms/substitutions (with objects as types/contexts) and then think of a functor into $T$, say $p : D \to T$ as a type system where the objects of $D$ are refinements of types in $T$ and the arrows are typing derivations. Then the functor can be thought of as "type erasure".

The general ideas there are very fibrational, for instance the fiber over a type $A$ in $T$ is a subtyping category over $A$. However, from this perspective type systems that are fibrations or opfibrations are very rare in programming languages, because they correspond to having principal types in a sense.

So I started thinking about why the Grothendieck construction fails for a general functor $p : D \to T$. First, we map the an object $A \in T$ to the fiber category $p^{-1}(A)$. For $f : A \to B$, if $p$ is a fibration we get a functor from $p^{-1}(B)$ to $p^{-1}(A)$ by taking the pullback and if its an opfibration we can go the other way by taking the pushforward. However, even assuming neither of these things we get that $f$ gives a profunctor from $p^{-1}(B)$ to $p^{-1}(A)$, where $f(a,b) = \{g \in D(a,b) | pg = f\}$.

So this works in general but the problem is that this doesn't generally extend to a functor from $T \to \text{Prof}^{\text{op}}$, because while identity is always preserved, composition may not be. The fact that composition is preserved, unrolling the coend, is equivalent to the statement that for every $\alpha : a \to c$ over $g \circ f$ where $f : A \to B, g : B \to C$ there exists (modulo some equivalence) $b, p(b) = B$ and $\alpha_f:a \to b, \alpha_g : b \to c$ over $f,g$ respectively, with $\alpha = \alpha_g \circ \alpha_f$.

I've never seen this property before, but it seems to me to be somewhat natural for programming language type systems since they are basically always presented syntactically in a "bottom-up" way. I'll call a functor that satisfies this property a "bottom-up" functor.

So if you have a bottom up functor you get a functor into $\text{Prof}^{\text{op}}$, and you can get back where you started by pulling back along a functor from what I'll call $(\text{Prof}^{op})_*$, whose objects are pairs of a category and an object in it $c \in C$ and arrows $c \in C \to d \in D$ are profunctors $R$ from $C$ to $D$ and an element of $R(d,c)$. Equivalently the objects are representable profunctors from $C \to 1$ and arrows from $c : C \to 1$ to $d : D \to 1$ are profunctors $R : D \to C$ and a natural transformation $\alpha : d \to c \circ R$.

Has anyone ever seen this construction before or the corresponding restriction on functors that it requires? And if I didn't mess it up are there any obvious nice consequences of it that I could use to prove things about functors that satisfy the property?

Answer 1

First of all, the phrase "Grothendieck construction" generally refers to the inverse construction, starting with a functor $T^{\mathrm{op}}\to \mathrm{Cat}$ and constructing a fibration $D\to T$.

Now, if you have an arbitrary functor $D\to T$, what you get is actually a normal lax functor $T^{\mathrm{op}} \to \mathrm{Prof}$, and conversely from any normal lax functor you can construct a functor $D\to T$. A proof can be found in Street's paper Powerful functors; he attributes the result to Benabou (unpublished).

At the end, Street has a characterization of those functors $D\to T$ that correspond to pseudofunctors into $\mathrm{Prof}$; they have the factorization property you mentioned, plus a uniqueness for that factorization up to zigzags. These functors are also exactly the exponentiable morphisms in $\mathrm{Cat}$, which was proven by Conduche and Giraud; thus they are sometimes called Conduche functors.