Let \(T\) be a 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 \(a_{1},a_{2}:A\). We write \(a_{1}\Rightarrow a_{2}:\mathord {\textnormal {\textsf {Type}}}(i)\) for the type of morphisms from \(a_{1}\) to \(a_{2}\).