[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
For the use of eta for sigma types, see Conor McBride's
Outrageous but meaningful coincidences
Higher-order unification modulo eta is used in a significant way there.
> Do you think that
> allowing it as a judgemental equality has significantly boosted the
> popularity of these systems?
Do you care what (A) I think or whether (B) "judgemental equality has
significantly boosted the popularity of these systems?" ;-)
(A) No clue.
(B) Let's ask an omniscient being in our afterlive.
Cheers,
Andreas
On 19.12.2017 10:10, Paul Blain Levy wrote:
[ 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
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
[email protected]
http://www.cse.chalmers.se/~abela/
