LevelLiterals.agda:11,19-30 Set (lsuc lzero ⊔ .ℓ) != Set when checking that the expression (A → ⊥) → ⊥ has type Set