** Next:** Definitions
** Up:** The LEGO library -
** Previous:** Quotient Types

There are two files, `relations.l`, and `relclosure.l`,
which give elementary and infinitary lemmas about the algebra of
relations. They pre-date the addition of primitive inductive types to
LEGO, so use impredicative encodings to get "System F"-like inductive
definitions.
In both files, a glaring omission is the failure to show that all the
operations on relations introduced are in fact extensional with
respect to `EQRel`. Much more could fruitfully be added.

*Conor McBride*

*11/13/1998*