the names ≤refl, ≤trans about agda-stdlib HOT 3 CLOSED

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.

from agda-stdlib.

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 _≤_.

from agda-stdlib.

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.

from agda-stdlib.