[Refractor] contradiction over ⊥-elim in Data.*.Relation.Binary.Lex.*

[jmougeot]

No description provided.

[jamesmckinna]

Suggest, however, also touching Data.Vec.Relation.Binary.Lex.Core to remove dependency on Data.Empty in favour of Relation.Nullary.Negation.Core.contradiction... not quite sure how this slipped through!?

Discovered a relevant change which should be committed before proceeding.

[jamesmckinna]

Additionally: fix Data.Vec.Relation.Binary.Lex.Core as suggested in line with the rest of these PRs, and mutatis mutandis, Data.List.Relation.Binary.Lex.Strict as well!

[jamesmckinna]

Final narrowing(s)?

[jamesmckinna]

Also https://github.com/jmougeot/agda-stdlib/blob/34d3fe0ce97d6252b277a547c68b1ad5f3cf2855/src/Data/List/Relation/Binary/Lex/Strict.agda#L14-L15:

open import Data.Empty using (⊥)
open import Data.Unit.Base using (⊤; tt)

can be streamlined to:

open import Data.Unit.Base using (tt)

and if you don't mind replacing tt with _ throughout (which it can, by eta-expansion for the record type ⊤...), even this can be deleted as well.

[jamesmckinna]

Yup, I think this will do fine.
Thanks for taking the trouble to cross-propagate changes between the List and Vec versions of these relations... interesting to see what's common and what's not!
cf. #2679

[jamesmckinna]

@JacquesCarette are you happy to approve and merge now?