# Monadicity of Beck-Chevalley bifibrations via a distributive law

Fix a category $B$ with pullbacks. The category of bifibrations over $B$ satisfying the Beck-Chevalley condition appears to be monadic over $\mathsf{Cat}/B$. Is this discussed somewhere in the literature?

Let $\mathsf{Fib}(B)$ be the category of fibrations and Cartesian functors over $B$. It's well-known that the forgetful functor $\mathsf{Fib}(B) \to \mathsf{Cat}/B$ is monadic; the induced monad $T$ is given by a comma category construction $T: (E \overset{p}{\to} B) \mapsto (B \downarrow p \to B)$. In fact, this monad is colax-idempotent. Dually, the monad $S: (E \overset{p}{\to} B) \mapsto (B \downarrow p \to B)$ is lax-idempotent, with algebras $\mathsf{OpFib}(B)$ given by opfibrations.

Thus far we have required no hypotheses on $B$. Now if $B$ has pullbacks, there appears to be (I have not checked all the coherence conditions) a (pseudo-)distributive law $TS \Rightarrow ST$ which takes a diagram $p(e) \to b \leftarrow b'$ to its pullback. And it looks like an algebra for the composite monad $ST$ is a bifibration (a functor which is simultaneously a fibration and an opfibration) satisfying the Beck-Chevalley condition over all pullback squares.

(Dually, if $B$ has pushouts, then there will be another distributive law in the other direction whose algebras will be bifibrations satisfying a dual Beck-Chevalley condition over pushout squares, but I've never heard of such a thing in nature.)

Not only does it seem good to know that the Beck-Chevalley condition arises from a monad, but this seems like a really cool example of a pseudo-distributive law! In general, it seems like these are a pain to work with because of the number of coherence conditions (even with the simplifications afforded by the (co)lax idempotency). Maybe that's why I've never heard of this one. But pullbacks can be strictified -- perhaps the pseudodistributive law can also be strictified?