Setoid version of indexed containers. (#1511)

* Setoid version of indexed containers.

Following the structure for non-indexed containers.

* An example for indexed containers: multi-sorted algebras.

This tests the new setoid version of indexed containers.

* Brought code up to date

* Added CHANGELOG entry

---------

Co-authored-by: MatthewDaggitt <[email protected]>

Author: andreasabel

CHANGELOG.md

@@ -75,6 +75,13 @@ New modules
   Relation.Binary.Construct.Interior.Symmetric
   ```
 
+* Pointwise and equality relations over indexed containers:
+  ```agda
+  Data.Container.Indexed.Relation.Binary.Pointwise
+  Data.Container.Indexed.Relation.Binary.Pointwise.Properties
+  Data.Container.Indexed.Relation.Binary.Equality.Setoid
+  ```
+
 Additions to existing modules
 -----------------------------
 
@@ -142,6 +149,11 @@ Additions to existing modules
   idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x
   ```
 
+* In `Data.Container.Indexed.Core`:
+  ```agda
+  Subtrees o c = (r : Response c) → X (next c r)
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   nonZeroIndex : Fin n → ℕ.NonZero n

doc/README/Data.agda

@@ -218,7 +218,8 @@ import README.Data.Vec.Relation.Binary.Equality.Cast
 -- monad, least fixed point, etc.) can be used
 
 import README.Data.Container.FreeMonad
-import README.Data.Container.Indexed
+import README.Data.Container.Indexed.VectorExample
+import README.Data.Container.Indexed.MultiSortedAlgebraExample
 
 -- Wrapping n-ary relations into a record definition so type-inference
 -- remembers the things being related.