1 files changed, 25 insertions, 23 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 245af6d..88191d6 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
 
 public export
 algebraOver : (sig : Signature) -> (U : sig.T -> Type) -> Type
@@ -30,25 +30,29 @@ public export
 record RawAlgebraWithRelation (0 sig : Signature) where
   constructor MkRawAlgebraWithRelation
   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) (0 rel : IRel a.U) where
+record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
   constructor MkIsAlgebra
-  equivalence : IEquivalence a.U rel
+  equivalence : IndexedEquivalence sig.T a.U
   semCong     : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity}
-    -> Pointwise rel tms tms' -> rel 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
   constructor MkAlgebra
   raw        : RawAlgebra sig
-  0 relation : IRel raw.U
-  algebra    : IsAlgebra sig raw relation
+  algebra    : IsAlgebra sig raw
+
+public export 0
+(.relation) : (0 a : Algebra sig) -> (t : sig.T) -> Rel (a.raw.U t)
+(.relation) a = IndexedEquivalence.relation a.algebra.equivalence
 
 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
 (.rawWithRelation) : Algebra sig -> RawAlgebraWithRelation sig
@@ -69,7 +73,7 @@ public export
 record Homomorphism {0 sig : Signature} (a, b : Algebra sig)
   where
   constructor MkHomomorphism
-  func : IFunc a.raw.U b.raw.U
+  func : (t : sig.T) -> a.raw.U t -> b.raw.U t
   homo : IsHomomorphism a b func
 
 public export
@@ -77,7 +81,7 @@ idIsHomo : {a : Algebra sig} -> IsHomomorphism a a (\_ => Basics.id)
 idIsHomo = MkIsHomomorphism
   (\_ => id)
   (\op, tms =>
-    (a.algebra.equivalence _).equalImpliesEq $
+    reflect (index a.setoid _) $
     sym $
     cong (a.raw.sem op) $
     mapId tms)
@@ -87,19 +91,17 @@ idHomo : {a : Algebra sig} -> Homomorphism a a
 idHomo = MkHomomorphism _ idIsHomo
 
 public export
-compIsHomo : {a, b, c : Algebra sig} -> {f : IFunc b.raw.U c.raw.U} -> {g : IFunc a.raw.U b.raw.U}
+compIsHomo : {a, b, c : Algebra sig}
+  -> {f : (t : sig.T) -> b.raw.U t -> c.raw.U t} -> {g : (t : sig.T) -> a.raw.U t -> b.raw.U t}
   -> IsHomomorphism b c f -> IsHomomorphism a b g -> IsHomomorphism a c (\i => f i . g i)
 compIsHomo fHomo gHomo = MkIsHomomorphism
-  (\t => fHomo.cong t . gHomo.cong t)
-  (\op, tms =>
-    (c.algebra.equivalence _).transitive
-      (fHomo.cong _ $ gHomo.semHomo op tms) $
-    (c.algebra.equivalence _).transitive
-      (fHomo.semHomo op (map g tms)) $
-    (c.algebra.equivalence _).equalImpliesEq $
-    sym $
-    cong (c.raw.sem op) $
-    mapComp tms)
+  { cong = \t => fHomo.cong t . gHomo.cong t
+  , semHomo = \op, tms => CalcWith (index c.setoid _) $
+    |~ f _ (g _ (a.raw.sem op tms))
+    ~~ f _ (b.raw.sem op (map g tms))           ...(fHomo.cong _ $ gHomo.semHomo op tms)
+    ~~ c.raw.sem op (map f (map g tms))         ...(fHomo.semHomo op _)
+    ~~ c.raw.sem op (map (\i => f i . g i) tms) .=<(cong (c.raw.sem op) $ mapComp tms)
+  }
 
 public export
 compHomo : {a, b, c : Algebra sig} -> Homomorphism b c -> Homomorphism a b -> Homomorphism a c