Add properties of non-divisibility to `Algebra.Properties.Magma.Divisibility`

jamesmckinna commented 2 months ago

Fixes #2306

NB.

is it an issue that Relation.Binary.Definitions._Respects₂_ seems to exchange 'left' and 'right' in its left/right projections? UPDATED: #2471
is it an issue (possible renaming/deprecation?) that the existing ∣∣-resp*-≈ lemmas concerning _∣∣_ all explicitly mention the equality _≈_, while none of the others (new, and existing) do? cf. #2341 Is this the occasion to remedy that state of affairs (in whichever direction we think: @MatthewDaggitt 's preference on that issue is to retain the symbol, so some additional renaming/deprecation would be necessary here...) UPDATED now FIXED, but it does feel like a lot of extra 'ink'?

JacquesCarette commented 2 months ago

Yes, I'd say that both points you raise are bugs that should be fixed (but in separate PRs). Make new issues?

jamesmckinna commented 2 months ago

Yes, I'd say that both points you raise are bugs that should be fixed (but in separate PRs). Make new issues?

Well, the second is somehow already covered by the quoted issue (I'm not clear about the history of these things, nor how these examples here somehow slipped through the net thrown by #2341 ?)

I've updated the preamble to link to a new issue for the first one.

agda / agda-stdlib

Add properties of non-divisibility to `Algebra.Properties.Magma.Divisibility` #2469