Subset Types

Among the objects of mathematics we consider are propositions. For example, 0=_N0 and 0<1 are true propositions about the primitive type N. We also consider propositional forms such as x=_Ny or x<y. These are sometimes called predicates.

The type of all (small) propositions is Prop. Propositional functions on a type A are elements of the type $A\rightarrow Prop$.

We also need types that can be restricted by predicates such as {x=N | x=0 or x=1}. This type behaves like the Booleans.

The general formation rule is this. If A is a type and $B:A\rightarrow Prop$, then $\{x:A \vert B(x)\}$ is a subtype of A.

The elements of $\{x:A \vert B(x)\}$ are those a in A for which B(a) is true.

Sometimes we state the formation in terms of predicates, so if P is a proposition for any x in A, then $\{x:A \vert P\}$ is a subtype of A.

We clearly have $\{x:A \vert P\} \subseteq A$.