Issue546.err

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