[TYPES] judgemental eta for function types

[Paul Blain Levy]

Dear all,

I have a question about systems like Coq and Agda that are based on
intensional type theory, and the way they treat the eta-law for
dependent function  types, including types of the form A->B and A*B and
1.  I have been told that they allow this eta-law as a judgemental
equality, not just propositional.  (By constrast, the eta-law for types
such as A+B and 0 is allowed as only as a propositional equality, in
order to keep judgements decidable, and allegedly for philosophical
reasons too.)

My question is, how useful is this facility (judgemental eta-law for
function types) in practice?  Can you give me examples of the ways that
users commonly make use of it?  To put the question differently, if the
eta-law for function types were available only as a propositional
equality, how inconvenient would that be for users?  Do you think that
allowing it as a judgemental equality has significantly boosted the
popularity of these systems?

Regards,

Paul