Add category laws for sublists

[andreasabel]

Data.List.Relation.Binary.Sublist.Setoid defines the preorder of order-preserving embeddings of lists,

⊆-isPreorder : IsPreorder _≋_ _⊆_
⊆-isPreorder = record
  { isEquivalence = ≋-isEquivalence
  ; reflexive     = ⊆-reflexive
  ; trans         = ⊆-trans
  }

but it does not prove the category laws, which are very useful if one wants to use sublist-proofs as renamings in lambda calculus. These laws would be:

• left unit: ⊆-trans ⊆-refl = id
• right unit
• associativity of ⊆-trans

Further, it would be useful to have the functor laws for Data.List.Relation.Binary.Sublist.Propositional.lookup in Data.List.Relation.Binary.Sublist.Propositional.Properties:

• identity: lookup ⊆-refl = id
• composition: lookup (⊆-trans p q) = lookup q . lookup p

[jamesmckinna]

Amazed that this hasn't been closed in the last 5 years!?

... and ahead of any effort to knock this off, @andreasabel do you have code of your own which you might like to contribute?

UPDATED: as with all proofs of higher-dimensional properties (of setoids), the need to delegate to the corresponding property of the the underlying setoid is... frustratingly fiddly. Esp. as the definition of ⊆-trans has subtly different definitional properties in the Setoid vs. Propositional case... so this is more work than I'd initially imagined. Sigh...

... And the work has already been done in the Propositional case... so only associativity remains to do (groan). Now done!