The Agda language supports eta equality for (non-(co)inductive) record types:

open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

eta : {A : Set} {B : A → Set} (x : Σ A B) → x ≡ (fst x , snd x)
eta x = refl

This was present since the first released of Agda 2 (see https://github.com/agda/agda/commit/1ac70d3ec0fc5151c71f9bdc8e8ebf8ea00ccd5c).

Likewise, Coq supports eta equality for records with primitive projections (but not for the unit type). However, primitive projections were only added to Coq in version 8.5, from 2016 (https://coq.inria.fr/news/coq-85-is-out.html).

My question: What was the first proof assistant to feature eta-equality for record types? Was there any language before Agda with this feature or was Agda really the first? Are there any publications that describe it?

  • 1
    $\begingroup$ I am not sure if this is the first (so I'm leaving a comment), but Nuprl has always supported the eta law for its sigma types; this goes back to 1985-ish, I suppose. But around the same time I think there was also an implementation of type theory in Gothenburg that I haven't been able to learn anything specific about. Maybe someone knows? $\endgroup$ Commented Dec 21, 2022 at 14:53
  • 1
    $\begingroup$ I would say an historically important reference here is Abel and Coquand's Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs. You have plenty of references there on how people have tried implementing η-equality for record types (or what they call strong sums). $\endgroup$ Commented Dec 21, 2022 at 18:32
  • 1
    $\begingroup$ @Meven: Ah excellent, that paper's related work section is indeed a very valuable resource. It pointed me in particular to this paper by Robin Adams from 2001, which is the earliest reference that I could find so far: citeseerx.ist.psu.edu/… $\endgroup$
    – Jesper
    Commented Dec 21, 2022 at 18:44
  • 2
    $\begingroup$ It's hard to find things about Automath - you should ask Freek directly. There are all sorts of wonders in there that people forget about. $\endgroup$ Commented Dec 21, 2022 at 23:55
  • 3
    $\begingroup$ I just found the following sentence in Thierry's 1991 paper on conversion checking: "It seems possible to extend the proof in the case where there is a dependent sum of types, and surjective pairing. The only changes are in the notion of weak head-normal form and the definition of => and <=>." So at least people were already considering the notion for a long time! So I really wonder why it took so long to get it into our implementations. $\endgroup$
    – Jesper
    Commented Dec 22, 2022 at 14:08


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.