|Next||Types Are Theorems; Programs Are Proofs||30|
Types like Int, Bool, etc. are known to be inhabited
They play the role of axioms in logic
For example, is a -> (a, Int) inhabited?
\a -> (a, 3) :: a -> (a, Int)
Similarly, if I is some axiom, then a → a ∧ I is a theorem