search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
459 stars 141 forks source link

Algebra structures without eta #1137

Closed felixwellen closed 3 months ago

felixwellen commented 5 months ago

I deactivated the eta for the records IsCommAlgebra and AlgebraStr and fixed the problems it causes. This does not seem to have tc speed impact, but I think it is still better because type checking will fail in a situation where two Algebra's are normalized for comparison (instead of taking forever).

felixwellen commented 5 months ago

depends on #1130

felixwellen commented 3 months ago

outdated experiment -> closing