1 files changed, 20 insertions, 27 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 6e39612..31b25b4 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -1,12 +1,12 @@
 module Soat.FirstOrder.Algebra
 
-import Data.Morphism.Indexed
 import Data.Setoid.Indexed
 import public Soat.Data.Product
 import Soat.FirstOrder.Signature
 
+import Syntax.PreorderReasoning.Setoid
+
 %default total
-%hide Control.Relation.Equivalence
 
 infix 5 ~>
 
@@ -24,15 +24,15 @@ public export
 record RawSetoidAlgebra (0 sig : Signature) where
   constructor MkRawSetoidAlgebra
   raw        : RawAlgebra sig
-  0 relation : IRel raw.U
+  0 relation : (t : sig.T) -> Rel (raw.U t)
 
 public export
 record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
   constructor MkIsAlgebra
-  0 relation  : IRel a.U
-  equivalence : IEquivalence a.U relation
+  equivalence : IndexedEquivalence sig.T a.U
   semCong     : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
-    -> Pointwise relation tms tms' -> relation t (a.sem op tms) (a.sem op tms')
+    -> Pointwise equivalence.relation tms tms'
+    -> equivalence.relation t (a.sem op tms) (a.sem op tms')
 
 public export
 record Algebra (0 sig : Signature) where
@@ -41,12 +41,12 @@ record Algebra (0 sig : Signature) where
   algebra    : IsAlgebra sig raw
 
 public export 0
-(.relation) : (0 a : Algebra sig) -> IRel a.raw.U
-(.relation) a = a.algebra.relation
+(.relation) : (0 a : Algebra sig) -> (t : sig.T) -> Rel (a.raw.U t)
+(.relation) a = a.algebra.equivalence.relation
 
 public export
-(.setoid) : Algebra sig -> ISetoid sig.T
-(.setoid) a = MkISetoid a.raw.U a.relation a.algebra.equivalence
+(.setoid) : Algebra sig -> IndexedSetoid sig.T
+(.setoid) a = MkIndexedSetoid a.raw.U a.algebra.equivalence
 
 public export
 (.rawSetoid) : Algebra sig -> RawSetoidAlgebra sig
@@ -56,19 +56,16 @@ public export
 record (~>) {0 sig : Signature} (a, b : Algebra sig)
   where
   constructor MkHomomorphism
-  func    : (t : sig.T) -> a.raw.U t -> b.raw.U t
-  cong    : (t : sig.T) -> {tm, tm' : a.raw.U t}
-    -> a.relation t tm tm' -> b.relation t (func t tm) (func t tm')
+  func    : a.setoid ~> b.setoid
   semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
-    -> b.relation t (func t (a.raw.sem op tms)) (b.raw.sem op (map func tms))
+    -> b.relation t (func.H t (a.raw.sem op tms)) (b.raw.sem op (map func.H tms))
 
 public export
 id : {a : Algebra sig} -> a ~> a
 id = MkHomomorphism
-  { func    = \_ => id
-  , cong    = \_ => id
+  { func    = id a.setoid
   , semHomo = \op, tms =>
-    (a.algebra.equivalence _).equalImpliesEq $
+    reflect (index a.setoid _) $
     sym $
     cong (a.raw.sem op) $
     mapId tms
@@ -77,15 +74,11 @@ id = MkHomomorphism
 public export
 (.) : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
 (.) f g = MkHomomorphism
-  { func    = \t => f.func t . g.func t
-  , cong    = \t => f.cong t . g.cong t
+  { func    = f.func . g.func
   , semHomo = \op, tms =>
-    (c.algebra.equivalence _).transitive
-      (f.cong _ $ g.semHomo op tms) $
-    (c.algebra.equivalence _).transitive
-      (f.semHomo op (map g.func tms)) $
-    (c.algebra.equivalence _).equalImpliesEq $
-    sym $
-    cong (c.raw.sem op) $
-    mapComp tms
+    CalcWith (index c.setoid _) $
+    |~ f.func.H _ (g.func.H _ (a.raw.sem op tms))
+    ~~ f.func.H _ (b.raw.sem op (map g.func.H tms))   ...(f.func.homomorphic _ _ _ $ g.semHomo op tms)
+    ~~ c.raw.sem op (map f.func.H (map g.func.H tms)) ...(f.semHomo op $ map g.func.H tms)
+    ~~ c.raw.sem op (map ((f.func . g.func).H) tms)   .=<(cong (c.raw.sem op) $ mapComp tms)
   }