search

agda / cubical

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

No-eta for CommAlgebras #1130

Open felixwellen opened 1 month ago

felixwellen commented 1 month ago

Just an experiment to see if it helps with tc speed when CommAlgbras have no eta law.

felixwellen commented 3 weeks ago

tc speed seems to be only minimally affected: Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback check a bit more than a second faster and I didn't see anything with a bigger change.

felixwellen commented 3 weeks ago

It might make more of a difference to have no-eta for Algebras (because e.g. type checking CommAlgebra-homomorphism compositions should actually be about Algebras being equal...)