From b21e69503571272a5f35cf84c731994f3e921a3a Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 29 Nov 2022 14:36:13 +0000
Subject: Move indexed setoids and functions out of Soat.

---
 src/Soat/SecondOrder/Algebra.idr      | 3 ++-
 src/Soat/SecondOrder/Algebra/Lift.idr | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'src/Soat/SecondOrder')

diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 50b65e0..c506c85 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -1,10 +1,11 @@
 module Soat.SecondOrder.Algebra
 
+import Data.Morphism.Indexed
+import Data.Setoid.Indexed
 import Data.List.Elem
 
 import Soat.Data.Product
 import Soat.Data.Sublist
-import Soat.Relation
 import Soat.SecondOrder.Signature
 
 public export
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index 00d453a..b08eb0e 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -1,12 +1,13 @@
 module Soat.SecondOrder.Algebra.Lift
 
 import Data.List.Elem
+import Data.Morphism.Indexed
+import Data.Setoid.Indexed
 
 import Soat.Data.Product
 import Soat.Data.Sublist
 import Soat.FirstOrder.Algebra
 import Soat.FirstOrder.Term
-import Soat.Relation
 import Soat.SecondOrder.Algebra
 import Soat.SecondOrder.Signature.Lift
 
-- 
cgit v1.2.3