Two-Sided Fibration

A 2-Sided Displayed Category $E\to A\times B$ is a 2-sided fibration if:

• For every $u:A(a,b)$, $x:B$, and $e:E_{b,x}$, there exists a $B$ vertical Cartesian lift $(u^{*}(e):E_{a,x},f:E_{u,\mathrm{id}}(u^{*}(e),e))$
• For every $a:A$, $x,y:B$, and $e:E_{a,x}$, there exists an $A$ vertical Cocartesian lift $(u_{!}(e):E_{a,y},f:E_{\mathrm{id},u}(e,u_{!}(e)))$.
• For every $u:A(a,b)$, $v:B(x,y)$, $e:E_{b,x}$ and cartesian/opcartesian composite $u^{*}(e)\to e\to v_{!}(e):E_{u,v}$, the canonical map $v_{!}(u^{*}(e))\to u^{*}(v_{!}(e))$ is a vertical isomorphism.

See Weinberger, Jonathan. “Two-Sided Cartesian Fibrations of Synthetic $(\infty,1)$-Categories,” March 12, 2024. https://doi.org/10.48550/arXiv.2204.00938. for a better, definition: in particular, Proposition 4.7 is much better!

In particular, we want cartesian morphisms to be stable under cobase change, and cocartesian morphisms to be stable under base change.

As bimodules

Two-sided fibrations are sort of like Bimodules; this analogy is made precise by considering the Arrow Category as a Monad in the Bicategory of Spans on $\mathrm{Cat}$, though this is quite dubious due to H-Level reasons.

References

• TwoSidedFibration.v
• Loregian, Fosco, and Emily Riehl. “Categorical Notions of Fibration.” Expositiones Mathematicae 38, no. 4 (December 2020): 496–514. https://doi.org/10.1016/j.exmath.2019.02.004.
• Categorical Logic and Type Theory, definition 9.1.5
• Von Glehn, Tamara. “Polynomials and Models of Type Theory,” June 30, 2015. https://doi.org/10.17863/CAM.16245.