confusion with the `reflexive` word

[mechvel]

Relation.Binary.Structures is parameterized by _≈_ : Rel A ℓ, and it puts

record IsEquivalence : Set (a ⊔ ℓ) where 
 field                                                                           
     refl  : Reflexive _≈_              
     ...                                                                                                                 
  reflexive : _≡_ ⇒ _≈_                                                           

Further, Algebra.Properties.Monoid.Divisibility (suggested by myself) implements

∣-reflexive : _≈_ ⇒ _∣_                                                            
∣-reflexive x≈y = ε , trans (identityˡ _) x≈y 

According to the standard library style, this probably needs to be

∣-reflexive≈ : _≈_ ⇒ _∣_    --  _∣_ is reflexive by _≈_
...
∣-reflexive : _≡_ ⇒ _∣_

(where the latter proof can be derived from the former). Am I missing something? Has standard library any more confusions with reflexive ?

[MatthewDaggitt]

So the current convention is that any proof of the type Reflexive is named refl and any proof of the type _≈_ ⇒ _R_ is named reflexive. Note this actually the opposite way around to the naming convention in Relation.Binary.Definitions where the more general name has the shorter name e.g. Trans vs Transitive and Sym vs Symmetric. I've tried to have a go at fixing this in the past, but it's impossible without breaking backwards compatibility in a major way! So we're pretty much stuck with that.

The convention for adding the equality relation to the end of the name of proofs of the form _≈_ ⇒ _R_ is that we only do so when the there are multiple different equality relations used in the same file. This is a very rare occurrence and the only place I can think that we currently do so is in Data.Rational.Unnormalised. So no it shouldn't be named ∣-reflexive-≈ (and certainly not ∣-reflexive≈!).

[gallais]

So we're pretty much stuck with that.

Should we start collating a wishlist for stdlib 2.0? Edit: oh, we already have a milestone for that. :D

[MatthewDaggitt]

We've decided that this decision is too deeply embedded into the library to change now.

[wenkokke]

We could possibly rename reflexive to fromPropositional or from-≡ to reflect that it’s a coercion.