Does Agda have definitional eta for sigma types?
Conversation
IIRC yes, but it can be disabled
2
3
Yeah! This is the part of the docs that talks about it:
agda.readthedocs.io/en/latest/lang
The sigma type from the stdlib is defined here - note that it doesn't disable the eta rules: agda.github.io/agda-stdlib/Ag