LEGO now supports small impredicative -types. To enable the alternative formation rule for small -types
you need to initialise either
For a discussion on -types and existential types, see pages 41 - 43 in Computation and Reasoning. See pages 32 - 33 in Computation and Reasoning for more information about predicative universes and the reflection principle.
The syntax for Records has changed, Constructors are now called Fields e.g.,