1 files changed, 55 insertions, 0 deletions
diff --git a/src/Data/Setoid.idr b/src/Data/Setoid.idr
new file mode 100644
index 0000000..8014bac
--- /dev/null
+++ b/src/Data/Setoid.idr
@@ -0,0 +1,55 @@
+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