Issue485.agda:6,14-15
Set₁ != Set
when checking that the expression A has type _2 f A