Next: Basic properties
Up: The LEGO library -
Previous: Specification and development of
This section contains modules which have been developed in pure Martin
Löf type theory i.e., without using UTT's impredicative
extension.
Conor McBride
11/13/1998