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