SortDependingOnIndex.agda:6,6-9
The sort of Bad cannot depend on its indices in the type (l :
Level) → Set l
when checking the definition of Bad