All Questions
Tagged with agda eta-equality
3
questions
7
votes
0
answers
195
views
What was the first proof assistant with eta equality for records?
The Agda language supports eta equality for (non-(co)inductive) record types:
...
- 506
22
votes
2
answers
409
views
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 ...
- 771
8
votes
1
answer
287
views
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 ...
- 1,053