IrrelevantModuleParameter.agda:4,7-8
Variable A is declared irrelevant, so it cannot be used here
when checking that the expression A has type Set (_0 _)