to express that \(\divi\) is a proof-object for the division theorem, that is, an element of the type representing the division theorem. When propositions are represented as types, the \(\forall\)-quantifier is identified with the dependent function space former (or general cartesian product) \(\Pi\), the \(\exists\)-quantifier with the dependent pairs type former (or general disjoint sum) \(\Sigma\), conjunction \(\wedge\) with cartesian product \( \times \), the identity relation = with the type former \(\I\) of proof-objects of identities, and the greater than relation \(&gt;\) with the type former \(\GT\) of proof-objects of greater-than statements. Using “type-notation” we thus write