Define indexed relations and equivalence records.

1 files changed, 75 insertions, 0 deletions

diff --git a/src/Soat/Relation.idr b/src/Soat/Relation.idr
new file mode 100644
index 0000000..475022d
--- /dev/null
+++ b/src/Soat/Relation.idr
@@ -0,0 +1,75 @@
+module Soat.Relation
+
+import 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
+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
+
+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) -> Soat.Relation.Equivalence (x i) (rel i)
+
+public export
+record ISetoid (a : Type) where
+  constructor MkISetoid
+  0 U           : a -> Type
+  0 rel         : IRel U
+  0 equivalence : IEquivalence U rel