search

agda / cubical

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

Pulling back an equivalence relation along a function #876

Closed MatthiasHu closed 2 years ago

MatthiasHu commented 2 years ago

This PR is a small contribution that shows that equivalence relations can be pulled back along functions.

felixwellen commented 2 years ago

I don't get the name "on". Maybe it would be better to be more verbose?

MatthiasHu commented 2 years ago

I took the name from Haskell: https://hackage.haskell.org/package/base-4.16.3.0/docs/Data-Function.html#v:on

But I understand that it is not optimal. Would it be an option to give the module a name (such as PulledBackRelation) so that one can write the following?

_~_ = ...

_~'_ = on fst _~_
  where open PulledBackRelation
felixwellen commented 2 years ago

Hm. So "on" means "along"? If I read "on fst R" somewhere, I would have no idea what it is about. What about just renaming "on" to "pulledbackRel" or "relPullback" or something like this?

MatthiasHu commented 2 years ago

Ok, I went with pulledbackRel.