search

UniMath / agda-unimath

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

Idea: use coherently invertible maps as default notion of equivalence #946

Open fredrik-bakke opened 11 months ago

fredrik-bakke commented 11 months ago

This is useful because it can give definitional computation laws for the inverse. It will take a large effort to refactor the greater library, but perhaps it is possible to start with a smaller refactoring to at least instate this as the default for future contributions. On the other hand, having two competing defaults may be detrimental to the quality and usability of the library, so we should discuss this rigorously before attempting to implement it.

fredrik-bakke commented 8 months ago

it would be very useful to implement #1030 before we undertake this refactoring. This will let us see if the refactoring leads to a performance improvement.