Move indexed setoids and functions out of Soat.

1 files changed, 36 insertions, 0 deletions

diff --git a/src/Data/Setoid/Indexed.idr b/src/Data/Setoid/Indexed.idr
new file mode 100644
index 0000000..df5606d
--- /dev/null
+++ b/src/Data/Setoid/Indexed.idr
@@ -0,0 +1,36 @@
+module Data.Setoid.Indexed
+
+import public Data.Setoid
+
+%default total
+
+public export
+IRel : {a : Type} -> (a -> Type) -> Type
+IRel {a = a} x = (i : a) -> x i -> x i -> Type
+
+public export
+IReflexive : {a : Type} -> (x : a -> Type) -> IRel x -> Type
+IReflexive x rel = (i : a) -> Reflexive (x i) (rel i)
+
+public export
+ISymmetric : {a : Type} -> (x : a -> Type) -> IRel x -> Type
+ISymmetric x rel = (i : a) -> Symmetric (x i) (rel i)
+
+public export
+ITransitive : {a : Type} -> (x : a -> Type) -> IRel x -> Type
+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) -> Setoid.Equivalence (x i) (rel i)
+
+public export
+record ISetoid (a : Type) where
+  constructor MkISetoid
+  0 U         : a -> Type
+  0 relation  : IRel U
+  equivalence : IEquivalence U relation
+
+public export
+isetoid : (a -> Type) -> ISetoid a
+isetoid u = MkISetoid u (\_ => Equal) (\_ => equiv)