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