From 3c200003925d2fc623c86f19706bcca7411adc76 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 5 Dec 2022 13:08:39 +0000
Subject: Define setoid reindexing.

---
 src/Data/Setoid/Indexed/Definition.idr | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/Data/Setoid/Indexed/Definition.idr b/src/Data/Setoid/Indexed/Definition.idr
index d50af06..cf2bb3d 100644
--- a/src/Data/Setoid/Indexed/Definition.idr
+++ b/src/Data/Setoid/Indexed/Definition.idr
@@ -61,6 +61,18 @@ index x i = MkSetoid
     }
   }
 
+public export
+reindex : (a -> b) -> IndexedSetoid b -> IndexedSetoid a
+reindex f x = MkIndexedSetoid
+  { U = x.U . f
+  , equivalence = MkIndexedEquivalence
+    { relation   = \i => x.equivalence.relation (f i)
+    , reflexive  = \i => x.equivalence.reflexive (f i)
+    , symmetric  = \i => x.equivalence.symmetric (f i)
+    , transitive = \i => x.equivalence.transitive (f i)
+    }
+  }
+
 namespace ToSetoid
   public export
   irrelevantCast : (0 b : a -> Type) -> IndexedSetoid a
-- 
cgit v1.2.3