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