Next: Algebraic Structures and Up: Type Theory Preliminaries Previous: Propositions and Universes

## Subtypes and Finiteness

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.

karla@cs.cornell.edu
Wed Jul 2 08:55:38 EDT 1997