search

UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
222 stars 71 forks source link

Equality proofs and proofs of propositions in `elementary-number-theory` should be abstracted #1106

Open fredrik-bakke opened 7 months ago

fredrik-bakke commented 7 months ago

Discussed in https://github.com/UniMath/agda-unimath/discussions/1102

Originally posted by **fredrik-bakke** March 30, 2024 Since the carrier types are sets the proofs are already irrelevant so it seems reasonable to do this. On the other hand, the performance of the module is not currently a problem.

Note: This should be done as an isolated pull request. There may be some very exceptional instances where we do not want to abstract the proof because it, for instance, is particularly simple and has nice computational behavior, and that is okay.