OpenPublicPlusTypeError.agda:12,17-21 Set₂ != Set when checking that the expression Set₁ has type Set