On 29 December 2015 at 20:19, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote: > Question: which type theory do you claim to implement with this? I don't know. (Ulf added the incompatibility of using type in type and universe polymorphism. Maybe he had a good reason for it.) -- Andrés