search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
561 stars 234 forks source link

Add `Data.List.Relation.Binary.Sublist.Setoid` categorical properties #2385

Closed jamesmckinna closed 1 month ago

jamesmckinna commented 1 month ago

Fixes #816

Includes some tidying up refactoring wrt variables (leading to a lot of redundant module _ where declarations...) and imports.

UPDATED: rectification for consistency with existing proofs in Data.List.Relation.Binary.Sublist.Propositional:

Possible TODO:

jamesmckinna commented 1 month ago

I added 4 micro commits which could be squashed.

Many thanks for the tweaks! FTR, stdlib commits get squashed in any case, so no worries about the size... ;-)

andreasabel commented 1 month ago

Greetings from AIM XXXVIII in Swansea!

jamesmckinna commented 1 month ago

Most recent commits now rectify the Propositional proofs as instances of the Setoid ones... but the latter have explicit parametrisation on the proofs of xs⊆ ys etc., while the former are implicit...

... changing the latter would be breaking; but the former seems better suited to the proofs. Which one is 'right'?

JacquesCarette commented 1 month ago

Tried to merge, but the build failed at the HTML stage. So it's probably just bad luck, and it should be tried again.