Issue546.agda:16,7-9 ⊤ !=< (P i) of type Set when checking that the expression tt has type P i