NotLeqSort.agda:5,3-25 The type of the constructor does not fit in the sort of the datatype, since Set₁ is not less or equal than Set when checking the constructor err in the declaration of Err