Next: Algebraic Structures and
Up: Type Theory Preliminaries
Previous: Propositions and Universes
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.