[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Paul, On Tue, Dec 19, 2017 at 12:35 PM Paul Blain Levy <p.b.l...@cs.bham.ac.uk> 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? It might seem annecdotical, but it's quite useful in practice to have Σ A (fun x : A => P x) be convertible to Σ A P. It's not unusual for a user to declare a value of type Σ A P and to use it to inhabit Σ A (fun x : A => P x). It comes up with typeclass instances in practice for example. I also comes up in formalizations of structures based on functions where some primitives definitions eta-expand. Typically for composition of functions you will have [f ∘ id = (fun x => f x) = f], and it's neat to have it be definitional. The fact that function composition and identity form a monoid "strictly" or on the nose is used for example in [1] to show that the Yoneda translation of a category is a category with equations holding up-to definitional equality. … > 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? > > I can't judge how significant it is. Note that without a definitional equality for eta, in older Coq versions for example, users were typically adding the functional extensionality axiom to derive it. [1] The Definitional Side of the Forcing. G. Jaber et al.. https://hal.archives-ouvertes.fr/hal-01319066 Best, -- Matthieu