Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\), let \(A:\mathord {\textnormal {\textsf {Type}}}(i)\), and let \(B(x):\mathord {\textnormal {\textsf {Type}}}(i)\) under assumption \(x:A\). We say \(B\) is a left fibration if it is right orthogonal to the function \(\mathord {\textnormal {\textsf {d}}}^{1}:\Delta \lbrack 0\rbrack \rightarrow \Delta \lbrack 1\rbrack \).