Fibrewise Opposite of a Cartesian Fibration

Let $E\to B$ be a Cartesian Fibration. The fibrewise opposite $E^{\mathrm{op}}\to B$ is defined as a Displayed category with the following structure:

• Objects $E^{\mathrm{op}}_{x}=E_{x}$.
• Morphisms $E^{\mathrm{op}}_{f}(x^{\prime},y^{\prime})$ over $f:x\to y$ are defined as $E_{\mathrm{id}}(f^{*}(y^{\prime}),x^{\prime})$.
• Composition and identities are defined as usual, modulo some coherence.

This has the effect of taking the opposite all the Fibre Categories. Note that the fibrewise opposite is still a fibration over $B$; contrast this with the Total Opposite, which gives a Cocartesian Fibration over $B^{\mathrm{op}}$.

Via the Grothendieck construction

One other way to see how the fibrewise opposite arises is by passing to Indexed Categories via the Grothendieck Construction; in this setting, the fibrewise opposite takes an indexed category $\mathcal{E}:\mathcal{B}^{\mathrm{op}}\to\mathrm{Cat}$ and gives a new indexed category $\mathcal{E}^{\mathrm{op}}$ defined by

This explains why fibrewise op needs some sort of (co)cartesian structure; the opposite needs to only flip the vertical portions! This perspective is also rather nice from the perspective of Differentiating Telescopes and Differential Forms; when we take the fibrewise opposite, we are changing the order of integration when we take the Total Category.

Fibrewise opposites of non-cloven fibrations

The above construction assumes that the fibration is Cloven. There is a much more complicated version in Fibered Categories a La Jean Benabou that works for non-cloven fibrations. The basic idea is that a non-cloven fibration induces a factorisation of maps $f:\mathcal{E}(X,Y)$ into equivalence classes of maps of the form, quotiented up to vertical isomorphism.

The non-cloven fibrewise opposite replaces these with equivalence classes of maps of the form:

As an "opdisplayed" category

This feels like it should be related to symmetries in Displayed Type Theory, which only show up when we have double display. Perhaps it is useful to think of categories as Augmented Categories here?

Examples

Many "bidirectional" categories of interest arise via fibrewise opposites:

• The Category of Lenses is the fibrewise opposite of the Simple Fibration over the Category of Sets.
• Dialectica Categories are a series fibrewise opposites of a Composition of Displayed Categories $(\mathcal{E}\circ\mathcal{F}^{\mathrm{op}})^{\mathrm{op}}$, where $\mathcal{F}\to\mathem{E}\to\mathcal{B}$
• The Category of Polynomial Functors is the fibrewise opposite of the Family Fibration over the Category of Sets.