3 files changed, 3 insertions, 11 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index b8cbc0c..f002dec 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -12,21 +12,13 @@ public export 0
 algebraOver : (sig : Signature) -> (U : sig.T -> Type) -> Type
 algebraOver sig x = {t : sig.T} -> (op : Op sig t) -> x ^ op.arity -> x t
 
-public export 0
-algebraOver' : (sig : Signature) -> (U : sig.T -> Type) -> Type
-algebraOver' sig x = {t : sig.T} -> (op : Op sig t) -> map x op.arity `ary` x t
-
 public export
 record RawAlgebra (0 sig : Signature) where
-  constructor MakeRawAlgebra
+  constructor MkRawAlgebra
   0 U : sig.T -> Type
   sem : sig `algebraOver` U
 
 public export
-MkRawAlgebra : (0 U : sig.T -> Type) -> (sem : sig `algebraOver'` U) -> RawAlgebra sig
-MkRawAlgebra u sem = MakeRawAlgebra u (\o => uncurry (sem o))
-
-public export
 record RawAlgebraWithRelation (0 sig : Signature) where
   constructor MkRawAlgebraWithRelation
   raw        : RawAlgebra sig
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index d0b1b14..84ac436 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -67,7 +67,7 @@ parameters {0 x, y : RawAlgebraWithRelation sig}
 
 public export
 Coproduct : (x, y : RawAlgebra sig) -> RawAlgebra sig
-Coproduct x y = MakeRawAlgebra
+Coproduct x y = MkRawAlgebra
   { U   = CoproductSet sig x.U y.U
   , sem = Call
   }
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 4a51f94..eaa2da2 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -127,7 +127,7 @@ namespace Rel
 
 public export
 Free : (0 V : sig.T -> Type) -> RawAlgebra sig
-Free v = MakeRawAlgebra (Term sig v) Call
+Free v = MkRawAlgebra (Term sig v) Call
 
 public export
 FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U) ((~=~) v.relation)