2-Sided Displayed Category

A 2-sided displayed category $\mathcal{E}\rightarrowtriangle C\times D$ is a category displayed over $C\times D$. We can also give an "elementary" definition where there is a space of objects $\mathem{E}_{0}\to\mathcal{C}_{0}\to\mathcal{D}_{0}\to\mathcal{U}$; this is the approach taken by Unimath.

References

• TwoSidedDispCat.v