3 files changed, 25 insertions, 7 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 982e54e..df5223f 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -38,10 +38,25 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where
 
 public export
 record Algebra (0 sig : Signature) where
-  constructor MkAlgebra
+  constructor MakeAlgebra
   raw        : RawAlgebra sig
   algebra    : IsAlgebra sig raw
 
+public export
+MkAlgebra : (U : IndexedSetoid sig.T)
+  -> (sem : {t : sig.T} -> (op : Op sig t) -> index (Product U) op.arity ~> index U t)
+  -> Algebra sig
+MkAlgebra u sem = MakeAlgebra
+  { raw     = MkRawAlgebra
+    { U   = u.U
+    , sem = \op => (sem op).H
+    }
+  , algebra = MkIsAlgebra
+    { equivalence = u.equivalence
+    , semCong     = \op => (sem op).homomorphic _ _
+    }
+  }
+
 public export 0
 (.relation) : (0 a : Algebra sig) -> (t : sig.T) -> Rel (a.raw.U t)
 (.relation) a = a.algebra.equivalence.relation
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 548beed..041d650 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -93,7 +93,7 @@ CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
 
 public export
 CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig
-CoproductAlgebra x y = MkAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra
+CoproductAlgebra x y = MakeAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra
 
 public export
 injectLHomo : x ~> CoproductAlgebra x y
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 2042d2f..a53e6b0 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -105,17 +105,20 @@ namespace Rel
     , transitive = \t, x, y, z => tmRelTrans eq.transitive
     }
 
+  public export
+  Term : (0 sig : Signature) -> (V : IndexedSetoid sig.T) -> IndexedSetoid sig.T
+  Term sig v = MkIndexedSetoid (Term sig v.U) (tmRelEq v.equivalence)
+
 public export
 Free : (0 V : sig.T -> Type) -> RawAlgebra sig
 Free v = MkRawAlgebra (Term sig v) Call
 
 public export
-FreeIsAlgebra : (v : IndexedSetoid sig.T) -> IsAlgebra sig (Free v.U)
-FreeIsAlgebra v = MkIsAlgebra (tmRelEq v.equivalence) Call
-
-public export
 FreeAlgebra : IndexedSetoid sig.T -> Algebra sig
-FreeAlgebra v = MkAlgebra _ (FreeIsAlgebra v)
+FreeAlgebra v = MkAlgebra
+  { U   = Term sig v
+  , sem = \op => MkSetoidHomomorphism (Call op) (\_, _ => Call op)
+  }
 
 public export
 bindTermCong' : {a : Algebra sig} -> {env, env' : (t : sig.T) -> v t -> a.raw.U t}