Issue689.err

Issue689.agda:8,3-17
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 c in the declaration of Bad