 Of course, in traditional mathematical notation we would not write the type symbols, and we would write \(\times_{\varrho \varrho \varrho}z_{\varrho}x_{\varrho}\) as \(z \times x\) and write \(\textrm{INV}_{\varrho \varrho}z\) as \(z^{-1}\). Thus \(z^{-1}\) is defined to be that x such that \(z \times x = 1\). When Z is provably not 0, we will be able to prove \(\exists_1 x_{\varrho}[\times_{\varrho \varrho \varrho} \textrm{Z x}_{\varrho} = 1_{\varrho}]\) and \(Z \times Z^{-1} = 1\), but if we cannot establish that Z is not 0, nothing significant about \(Z^{-1}\) will be provable.