1 files changed, 2 insertions, 45 deletions
diff --git a/src/Soat/Relation.idr b/src/Soat/Relation.idr
index 6d6b691..9826d60 100644
--- a/src/Soat/Relation.idr
+++ b/src/Soat/Relation.idr
@@ -1,53 +1,10 @@
 module Soat.Relation
 
-import Control.Relation
+import public Data.Setoid
 
 %default total
 
 public export
-record Equivalence a (rel : Rel a) where
-  constructor MkEquivalence
-  refl  : Reflexive a rel
-  sym   : Symmetric a rel
-  trans : Transitive a rel
-
-public export
-equiv : Control.Relation.Equivalence a rel => Soat.Relation.Equivalence a rel
-equiv = MkEquivalence (MkReflexive reflexive) (MkSymmetric symmetric) (MkTransitive transitive)
-
-public export
-[refl'] (eq : Soat.Relation.Equivalence a rel) => Control.Relation.Reflexive a rel where
-  reflexive = reflexive @{eq.refl}
-
-public export
-[sym'] (eq : Soat.Relation.Equivalence a rel) => Control.Relation.Symmetric a rel where
-  symmetric = symmetric @{eq.sym}
-
-public export
-[trans'] (eq : Soat.Relation.Equivalence a rel) => Control.Relation.Transitive a rel where
-  transitive = transitive @{eq.trans}
-
-public export
-[equiv'] Soat.Relation.Equivalence a rel => Control.Relation.Equivalence a rel
-  using refl' sym' trans' where
-
-public export
-(.reflexive) : Soat.Relation.Equivalence a rel -> {x : a} -> rel x x
-(.reflexive) eq = reflexive @{eq.refl}
-
-public export
-(.symmetric) : Soat.Relation.Equivalence a rel -> {x, y : a} -> rel x y -> rel y x
-(.symmetric) eq = symmetric @{eq.sym}
-
-public export
-(.transitive) : Soat.Relation.Equivalence a rel -> {x, y, z : a} -> rel x y -> rel y z -> rel x z
-(.transitive) eq = transitive @{eq.trans}
-
-public export
-(.equalImpliesEq) : Soat.Relation.Equivalence a rel -> {x, y : a} -> x = y -> rel x y
-(.equalImpliesEq) eq Refl = eq.reflexive
-
-public export
 IRel : {a : Type} -> (a -> Type) -> Type
 IRel {a = a} x = (i : a) -> x i -> x i -> Type
 
@@ -65,7 +22,7 @@ ITransitive x rel = (i : a) -> Transitive (x i) (rel i)
 
 public export
 IEquivalence : {a : Type} -> (x : a -> Type) -> IRel x -> Type
-IEquivalence x rel = (i : a) -> Soat.Relation.Equivalence (x i) (rel i)
+IEquivalence x rel = (i : a) -> Setoid.Equivalence (x i) (rel i)
 
 public export
 record ISetoid (a : Type) where