[TYPES] judgemental eta for function types

[Andreas Abel]

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

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/