1 files changed, 0 insertions, 55 deletions
diff --git a/src/Data/Setoid.idr b/src/Data/Setoid.idr
deleted file mode 100644
index 8014bac..0000000
--- a/src/Data/Setoid.idr
+++ /dev/null
@@ -1,55 +0,0 @@
-module Data.Setoid
-
-import public Control.Relation
-
-%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
-record Setoid where
-  constructor MkSetoid
-  0 U         : Type
-  0 relation  : Rel U
-  equivalence : Data.Setoid.Equivalence U relation
-
-public export
-equiv : Control.Relation.Equivalence a rel => Data.Setoid.Equivalence a rel
-equiv = MkEquivalence (MkReflexive reflexive) (MkSymmetric symmetric) (MkTransitive transitive)
-
-public export
-[refl'] (eq : Data.Setoid.Equivalence a rel) => Reflexive a rel where
-  reflexive = reflexive @{eq.refl}
-
-public export
-[sym'] (eq : Data.Setoid.Equivalence a rel) => Symmetric a rel where
-  symmetric = symmetric @{eq.sym}
-
-public export
-[trans'] (eq : Data.Setoid.Equivalence a rel) => Transitive a rel where
-  transitive = transitive @{eq.trans}
-
-public export
-[equiv'] Data.Setoid.Equivalence a rel => Control.Relation.Equivalence a rel
-  using refl' sym' trans' where
-
-public export
-(.reflexive) : Data.Setoid.Equivalence a rel -> {x : a} -> rel x x
-(.reflexive) eq = reflexive @{eq.refl}
-
-public export
-(.symmetric) : Data.Setoid.Equivalence a rel -> {x, y : a} -> rel x y -> rel y x
-(.symmetric) eq = symmetric @{eq.sym}
-
-public export
-(.transitive) : Data.Setoid.Equivalence a rel -> {x, y, z : a} -> rel x y -> rel y z -> rel x z
-(.transitive) eq = transitive @{eq.trans}
-
-public export
-(.equalImpliesEq) : Data.Setoid.Equivalence a rel -> {x, y : a} -> x = y -> rel x y
-(.equalImpliesEq) eq Refl = eq.reflexive