Synthetic topos theory
[005A] Definition

Let \(U\) be a universe, let \(C\) be a \(U\)-logos, and let \(I\) be a partially ordered object in \(C\) with least and greatest elements. We say a morphism in \(C\) is a \(I\)-left fibration if it is internally right orthogonal to \(\mathord {\textnormal {\textsf {d}}}^{1}:\Delta _{I}\lbrack 0\rbrack \rightarrow \Delta _{I}\lbrack 1\rbrack \).