IrrelevantData.agda:9,11-12 Variable x is declared irrelevant, so it cannot be used here when checking that the expression x has type .A