This section contains modules which have been developed in pure Martin Löf type theory i.e., without using UTT's impredicative extension.
