Skip to main content

Questions tagged [eta-equality]

Things related to η-convertibility, η-expansion, η-reduction, and their use in simplifying proofs.

Filter by
Sorted by
Tagged with
22 votes
2 answers

In what intensional type theories can absurdity be made definitionally proof irrelevant?

Various type theories have, over the years, explored extending the definitional equality with a variety of eta-laws and various forms of proof irrelevance. Quite a lot of systems manage eta for ...
pigworker's user avatar
  • 771
9 votes
1 answer

Strong eta-rules for functions on sum types

I am wondering whether a rule like the following is consistent with decidable conversion and type-checking for dependent type theory: $$ \frac{f\, g : (x:\mathsf{bool}) \to C~x\quad f~\mathsf{tt} \...
Mike Shulman's user avatar
  • 3,060
8 votes
1 answer

When should I use `no-eta-equality` in Agda records?

In a recent development, I used the no-eta-equality attribute on a record. The motivation in that case was ad hoc: I noticed that I'd get better metavariable ...
James Wood's user avatar
  • 1,053
7 votes
0 answers

What was the first proof assistant with eta equality for records?

The Agda language supports eta equality for (non-(co)inductive) record types: ...
Jesper's user avatar
  • 486
3 votes
1 answer

What is the well-established η law for naturals?

Notation. means a general equality. Well, $η$ laws are usually judgmental, but sometimes we provide $η$ laws as theorems. To me $η$ rules are like vibes, because ...
ice1000's user avatar
  • 6,176
2 votes
1 answer

Eta-equality for records: the case of semigroups

Consider the following definition of a semigroup: ...
Jon's user avatar
  • 75