1

A set with elements of type $a$ typically is represented in type theory by $Set \ a: a \to bool$ or, as an algebraic expression $Set \ a: 2^a$.
The idea is that, for each element of the type $a$, you ask whether it is a member of your set. $2^a$ counts how many distinct subsets there are. For in...