  It is clear intuitively how we can explain type theory in set theory: a type is simply interpreted as a set, and function types \(A \rightarrow B\) can be explained using the set theoretic notion of function (as a functional relation, i.e. a set of pairs of elements). The type \(A \rightarrow o\) corresponds to the powerset operation.