5 files changed, 34 insertions, 12 deletions
diff --git a/src/Data/Setoid/Product.idr b/src/Data/Setoid/Product.idr
index 6693d40..b1e8ce3 100644
--- a/src/Data/Setoid/Product.idr
+++ b/src/Data/Setoid/Product.idr
@@ -101,6 +101,11 @@ wrapIntro []        = []
 wrapIntro (r :: rs) = r :: wrapIntro rs
 
 public export
+wrapFunc : (0 x : IndexedSetoid b) -> (0 f : a -> b)
+  -> Product (reindex f x) ~> reindex (map f) (Product x)
+wrapFunc x f = MkIndexedSetoidHomomorphism (\_ => wrap f) (\_, _, _ => wrapIntro)
+
+public export
 unwrapIntro : forall f . {0 rel : (i : b) -> Rel (x i)} -> {is : _} -> {0 xs, ys : x ^ map f is}
   -> Pointwise rel xs ys -> Pointwise (\i => rel (f i)) {is = is} (unwrap f xs) (unwrap f ys)
 unwrapIntro {is = []}        []        = []
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}
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index d80eeb1..8bbcf9e 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -26,11 +26,10 @@ project a ctx = MkRawAlgebra
 public export
 projectAlgebra : (0 sig : _) -> Algebra (lift sig) -> (ctx : List sig.T) -> Algebra sig
 projectAlgebra sig a ctx = MkAlgebra
-  { raw = project a.raw ctx
-  , algebra = MkIsAlgebra
-    { equivalence = (reindex (flip MkPair ctx) a.setoid).equivalence
-    , semCong     = \op => a.algebra.semCong ctx (MkOp (Op op.op)) . wrapIntro
-    }
+  { U   = a.setoidAt ctx
+  , sem = \op =>
+    a.semFunc ctx (MkOp (Op op.op)) .
+    index (wrapFunc (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) (MkPair [])) _
   }
 
 public export