3 files changed, 19 insertions, 12 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index f0b23ea..6f9389b 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -25,18 +25,22 @@ record RawSetoidAlgebra (0 sig : Signature) where
   0 relation : IRel raw.U
 
 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
+  0 relation  : IRel a.U
+  equivalence : IEquivalence a.U relation
   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 relation tms tms' -> 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) -> IRel a.raw.U
+(.relation) a = a.algebra.relation
 
 public export
 (.setoid) : Algebra sig -> ISetoid sig.T
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 736dc75..29a740f 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -73,11 +73,14 @@ Coproduct x y = MkRawAlgebra
   }
 
 public export
-CoproductIsAlgebra : IsAlgebra sig x rel -> IsAlgebra sig y rel'
+CoproductIsAlgebra : IsAlgebra sig x -> IsAlgebra sig y
   -> IsAlgebra sig (Coproduct x y)
-       ((~=~) (MkRawSetoidAlgebra x rel) (MkRawSetoidAlgebra y rel'))
 CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
-  { equivalence = \t => MkEquivalence
+  { relation =
+    (~=~)
+      (MkRawSetoidAlgebra x xIsAlgebra.relation)
+      (MkRawSetoidAlgebra y yIsAlgebra.relation)
+  , equivalence = \t => MkEquivalence
     { refl  = MkReflexive $ coprodRelRefl
         (\t => (xIsAlgebra.equivalence t).refl)
         (\t => (yIsAlgebra.equivalence t).refl)
@@ -90,7 +93,7 @@ CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
 
 public export
 CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig
-CoproductAlgebra x y = MkAlgebra _ _ $ CoproductIsAlgebra x.algebra y.algebra
+CoproductAlgebra x y = MkAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra
 
 public export
 injectLIsHomo : IsHomomorphism x (CoproductAlgebra x y) (\_ => Done . Left)
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index eaa2da2..45282cc 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -130,12 +130,12 @@ Free : (0 V : sig.T -> Type) -> RawAlgebra sig
 Free v = MkRawAlgebra (Term sig v) Call
 
 public export
-FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U) ((~=~) v.relation)
-FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call'
+FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U)
+FreeIsAlgebra v = MkIsAlgebra ((~=~) v.relation) (tmRelEq v.equivalence) Call'
 
 public export
 FreeAlgebra : ISetoid sig.T -> Algebra sig
-FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)
+FreeAlgebra v = MkAlgebra _ (FreeIsAlgebra v)
 
 public export
 bindTermCong' : {a : Algebra sig} -> {env, env' : IFunc v a.raw.U} -> {0 rel : IRel v}