I've been taking the ideas expressed in ["Functors are Type Refinement Systems"](http://noamz.org/papers/funts.pdf) 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?



Profunctorial Grothendieck Construction?
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](http://ncatlab.org/nlab/show/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](http://maths.mq.edu.au/~street/Pow.fun.pdf); 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](https://ncatlab.org/nlab/show/Conduch%C3%A9+functor).


