Add smart constructor for first-order algebras.refactor/strict

1 files changed, 8 insertions, 5 deletions

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}