[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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