Move indexed setoids and functions out of Soat.

2 files changed, 49 insertions, 0 deletions

diff --git a/src/Data/Morphism/Indexed.idr b/src/Data/Morphism/Indexed.idr
new file mode 100644
index 0000000..c271c90
--- /dev/null
+++ b/src/Data/Morphism/Indexed.idr
@@ -0,0 +1,13 @@
+module Data.Morphism.Indexed
+
+import Data.Setoid.Indexed
+
+public export
+IFunc : {a : Type} -> (x, y : a -> Type) -> Type
+IFunc {a} x y = (i : a) -> x i -> y i
+
+public export
+record IFunction {a : Type} (x, y : ISetoid a) where
+  constructor MkIFunction
+  func : IFunc x.U y.U
+  cong : (i : a) -> {u, v : x.U i} -> x.relation i u v -> y.relation i (func i u) (func i v)
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)