Elementary Fibration

A fibration $p:E\to B$ is elementary when $p$ is a faithful and conservative.

From the displayed perspective, this means that the homs $E_{f}(x,y)$ are all propositions, and that we can lift invertible maps. This means that the fibre categories are all posetal groupoids, or in other words: setoids!

References

• Streicher, Thomas. “Fibered Categories a La Jean Benabou.” arXiv, June 15, 2022. http://arxiv.org/abs/1801.02927.