Pulling back an equivalence relation along a function

[MatthiasHu]

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

[felixwellen]

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

[MatthiasHu]

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]

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]

Ok, I went with pulledbackRel.

[felixwellen]

Thanks! Looks good to me now.