1 files changed, 16 insertions, 1 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