From ce49914c213f798dd052229efe92633247fd4435 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 29 Nov 2022 14:57:29 +0000
Subject: Prove Pointwise forms a setoid.

---
 src/Soat/Data/Product.idr | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'src')

diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
index f392a2d..0cb5dda 100644
--- a/src/Soat/Data/Product.idr
+++ b/src/Soat/Data/Product.idr
@@ -192,6 +192,17 @@ namespace Pointwise
   pwTrans f []        []        = []
   pwTrans f (r :: rs) (s :: ss) = transitive r s :: pwTrans f rs ss
 
+  public export
+  pwEquivalence : IEquivalence x rel -> {is : _} -> Setoid.Equivalence (x ^ is) (Pointwise rel)
+  pwEquivalence eq = MkEquivalence
+    (MkReflexive $ pwRefl (\i => (eq i).refl))
+    (MkSymmetric $ pwSym (\i => (eq i).sym))
+    (MkTransitive $ pwTrans (\i => (eq i).trans))
+
+  public export
+  pwSetoid : ISetoid a -> List a -> Setoid
+  pwSetoid x is = MkSetoid (x.U ^ is) _ (pwEquivalence x.equivalence)
+
   -- Introductors and Eliminators
 
   public export
-- 
cgit v1.2.3