UnequalRelevance.agda:11,7-8 (A → A) !=< (.A → A) because one is a relevant function type and the other is an irrelevant function type when checking that the expression f has type .A → A