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?


1 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.

  • 6
    $\begingroup$ For another (unpublished) reference, Bénabou discusses these and other properties of "generalised fibrations" in Section 7 of "Distributors at Work" (lecture notes prepared by Thomas Streicher). $\endgroup$ Commented Aug 4, 2016 at 15:00
  • $\begingroup$ Is there established terminology for the correspondence between the two rather than the specific half of the correspondence that "Grothendieck construction" refers to? I've searched for "Grothendieck correspondence" but nothing relevant came up. $\endgroup$
    – Max New
    Commented Oct 25, 2016 at 20:32
  • $\begingroup$ I don't know of a short term for it. $\endgroup$ Commented Oct 25, 2016 at 21:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.