Equivalence Relations and Quotient Types

Hopcroft and Ullman say: ``A binary relation on a set is a set of pairs of elements in . If is in , then we are accustomed to seeing this fact written .''

In set theory a set of pairs can be defined in terms of its characteristic function . In type theory these sets are expressed as functions from into the propositions. In type theory all functions are computable, so we do not use maps into unless the set or relation is decidable.

A relation on is said to be:

1. reflexive iff for each in , ,
2. symmetric iff for each implies ,
3. transitive iff for each imply .

A reflexive, symmetric and transitive relation is called an equivalence relation. For an equivalence relation, we sometimes write and say .'' We sometimes also write as when stressing that is a function. The equivalence class of an element of under is the set denoted or . The equivalence classes of under are clearly disjoint or equal since if for then hence and by transitivity so The set of equivalence classes is a partition of . In set theory this structure is denoted and is called the quotient set of by . The map from to is called the canonical mapping of onto . It is common to think of the classes as new elements with equality between them defined by , i.e. .

If then we say that is functional on (or compatible with ) iff implies that Likewise for an (binary) operation on ; we say is functional wrt iff and implies

Quotient sets and structures are central to mathematics, but their representation in set theory is not suitable for computation because the elements of a quotient set are equivalence classes which are infinite objects. To remedy this ``computational defect'' of set theory, type theory uses the notion of a quotient type. Given a type and an equivalence relation on , there is a type called the quotient of by , written (or in fully expanded form). The elements of are the same as those of , but the equality relation on is .

In order to qualify as a function must be a function which is functional wrt . The canonical map is just the identity function, so the functionality theorem becomes is functional wrt iff

Here is another important fact about Nuprl's rules for the quotient type. The elements of are elements of so is a subtype of . Also knowing for is sufficient to conclude , but not conversely. That is, if we know , we need not know constructively that . (We can conclude this if is decidable.)

To understand this feature of the quotient rules, we need to point out that according to Martin-Löf's semantics, the computational content of equality propositions, , is trivial. The theory only records that these propositions are proved, but ignores the details. Let us call this the ``computational triviality of equality'' principle. To preserve this semantic principle in the presence of quotient types requires that the rules ``forget'' the computational information in a proof of when asserting .