agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
561 stars 234 forks source link

Move pointwise equality to `.Core` module #2335

Closed JacquesCarette closed 3 months ago

JacquesCarette commented 3 months ago

Closes #2331.

Also makes a few changes of imports that are related. Many of the places which look like this improvement might also help use other things from Relation.Binary.PropositionalEquality that should not be moved to .Core. (But it might make sense to split them off into their own lighter weight module.)