 where \(1\) is a one element type and \(\times\) denotes the cartesian product of two types. We note that dependent types introduce computation in types: the defining rules above are computation rules. For example, the result of computing \(A^3\) is \(A \times (A \times (A \times 1))\).