On 2015-10-09 08:48, Ashish Mishra wrote: > I am facing a pertinent issue while defining new LEVELS of Universes > using the BUILTIN pragmas of Agda . The mechanism used to introduce levels has changed: https://github.com/agda/agda/blob/2.4.2.4/CHANGELOG#L3134-L3147 https://github.com/agda/agda/blob/2.4.2.4/CHANGELOG#L1156-L1210 -- /NAD