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

* refactor: `variable` declarations and `contradiction`

* refactor: one more `contradiction`

* left- and right-unit lemmas

* left- and right-unit lemmas

* `CHANGELOG`

* `CHANGELOG`

* associativity; fixes #816

* Use cong2 to save rewrites

* Make splits for ⊆-assoc exact, simplifying the [] case

* Simplify ⊆-assoc not using rewrite

* Remove now unused private helper

* fix up names and `assoc` orientation; misc. cleanup

* new proofs can now move upwards

* delegate proofs to `Setoid.Properties`

---------

Co-authored-by: Andreas Abel <[email protected]>

Author: jamesmckinna

CHANGELOG.md

@@ -380,6 +380,18 @@ Additions to existing modules
   map-catMaybes         : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f)
   ```
 
+* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
+  ```agda
+  ⊆-trans-idˡ   : (trans-reflˡ : ∀ {x y} (p : x ≈ y) → trans ≈-refl p ≡ p) →
+                  (pxs : xs ⊆ ys) → ⊆-trans ⊆-refl pxs ≡ pxs
+  ⊆-trans-idʳ   : (trans-reflʳ : ∀ {x y} (p : x ≈ y) → trans p ≈-refl ≡ p) →
+                  (pxs : xs ⊆ ys) → ⊆-trans pxs ⊆-refl ≡ pxs
+  ⊆-trans-assoc : (≈-assoc : ∀ {w x y z} (p : w ≈ x) (q : x ≈ y) (r : y ≈ z) →
+                             trans p (trans q r) ≡ trans (trans p q) r) →
+                  (ps : as ⊆ bs) (qs : bs ⊆ cs) (rs : cs ⊆ ds) →
+                  ⊆-trans ps (⊆-trans qs rs) ≡ ⊆-trans (⊆-trans ps qs) rs
+  ```
+
 * In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
   ```agda
   map⁺ : f Preserves _≈_ ⟶ _≈′_ → as ⊆ bs → map f as ⊆′ map f bs