search

agda / cubical

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

Move _$_ from Reflection.Base to Foundations.Function #894

Closed ecavallo closed 1 year ago

ecavallo commented 2 years ago

It doesn't have anything to do with reflection (don't know why I put it there in the first place) and is generally useful.

The obstacle is that different functions called _$_ are defined elsewhere in the library, namely in Algebra.Ring.Base and Data.Graph.Base. We'd have to rename these.

mzeuner commented 2 years ago

Maybe we could use something like _$r_ for ring morphisms?

ecavallo commented 2 years ago

Yeah, I think there's already a _$a_ for algebras or something like that. For the graph homomorphisms it might be best to change it to match the Algebra conventions for homs.

felixwellen commented 2 years ago

I think I defined _$a_ but ended up not using it. But now that I think of it, I'm actually for using it and similar functions.