Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\). Then \(\mathcal {E}(i)\) satisfies directed univalence. That is, for any \(A,B:\mathcal {E}(i)\), the canonical function

\((A\Rightarrow B)\rightarrow (A\rightarrow B)\) induced by the axiom that \((X:\mathcal {E}(i))\mapsto X\) is a left fibration is an equivalence.