Issue216.agda:8,11-26 Set (lsuc i) != Set i when checking that the expression (R : Set i) → R has type Set i