errors/UnequalSorts.agda:8,7-11
Set1 != Set
when checking that the expression one' has type One