Open mechvel opened 6 months ago
Thanks for the suggestion, but looking at the search results, it's clear with the one exception in Relation.Binary.Properties
, the convention in the library is to have the equality afterwards.
Keeping this issue open to fix the proofs at: https://github.com/agda/agda-stdlib/blob/4676ad7f3e1f58f5aaa9c761a49098855153e0c1/src/Relation/Binary/Properties/Setoid.agda#L74-L81
For the three exceptions noted, I'd be prepared to leave them as is, precisely because _≉_
presupposes the equality relation as part of its definition, so in that sense these properties are not 'uniform' with the style of ad hoc provable 'respects' properties, but true by virtue of the definitions.
On that basis, I'd perhaps prefer to leave them as distinct?
In lib-2.0, Algebra.Properties.Magma.Divisibility
introduces the names
∣-respʳ
and∣∣-respʳ-≈
.I suggest to declare
∣∣-respʳ-≈
as obfuscated and to introduce∣∣-respʳ
instead.And to treat
∣∣-respˡ, ∣∣-resp-≈
similarly.The reasons are as follows.
1) A uniform denotation style is desirable.
2) It is clear for Magma that "
_∣_
respects" is about the equality of_≈_
as default (for_≡_
, one can usesubst
or to introduce∣-resp-≡
).And if one needs
∣-resp
with respect to some other relationfoo
, then it can be introduced∣-resp-foo
.