We use a natural notion of subtype. If is a type and is a propositional function, then denotes the type of all elements of satisfying . To know that we must build the element and find a proof of There is a subtle computational point about these sets, namely a function from to does not have access to a proof that holds when calculating its value .
A finite type is one which can be put into a 1-1 correspondence with ; its cardinality is . We write to mean that is finite. This means we can find a number and functions and such that such that and are inverses of each other; that is
The definition of 1-1 correspondence is in fun_1, and finiteness is in automata_2.
Here is an important fact about finite types. We say that a type is discrete iff there is a function such that in iff , that is, is discrete iff equality on is decidable.
Fact: If is finite, then it is discrete.
This is true because is discrete for any ; thus to decide , ask whether for the function witnessing finiteness.