  We have seen the analogy between the operation A \(\rightarrow\) A \(\rightarrow\) o on types and the powerset operation on sets. In set theory, the powerset operation can be iterated transfinitely along the cumulative hierarchy. It is then natural to look for analogous transfinite versions of type theory.