 In particular, in this system every proposition can be represented as a type: namely, the type of proofs of the proposition. Conversely, each type determines a proposition: namely, the proposition that the type in question is inhabited. So when we think of a certain type \(T\) as a proposition, we interpret the formula 