[TYPES] judgemental eta for function types

[Matthieu Sozeau]

Dear Paul,

On Tue, Dec 19, 2017 at 12:35 PM Paul Blain Levy <P.B.Levy at 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