All Questions
1
question
6
votes
1
answer
101
views
What are the typechecking differences between records and iterated sigma types in Agda?
If we have univalence at hand, the records and iterated sigma versions of some type will be equal. Still, there may be some important typechecking-related differences.
For example, it seems that one ...
- 161