the names ≤refl, ≤trans

[mechvel]

DecTotalOrder exports reflexive and trans. And these names are also exported by IsEquivalence for _≈_. Besides IsEquivalence and _≈_ are inside DecTotalOrder. This leads to a confusion.

It not this better to have ≤refl and ≤trans instead?

[MatthewDaggitt]

I agree that it would be far better to prefix all the ordering properties in the ordering records with the order and leave the equality properties with the standard name. For example isPartialOrder would export publicly refl : Reflexive _≈_ and ≤-refl : Reflexive _≤_.

However changing this now would break almost every piece of Agda code in existence. So unfortunately, unless someone important disagrees, I don't think this is going to get changed.

[WolframKahl]

At import (either direct or in one of my .Utils modules ...) I will always make sure that I get to use ≈-refl : Reflexive _≈_ and ≤-refl : Reflexive _≤_.

[MatthewDaggitt]

At import (either direct or in one of my .Utils modules ...) I will always make sure that I get to use ≈-refl : Reflexive ≈ and ≤-refl : Reflexive ≤.

I do the same. It is annoying, but sadly I think that this is one of these things that is going to have to stick around.