From fcd024cb01e484dc3c92212f4317b254bbd7580b Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 6 Dec 2022 16:18:29 +0000
Subject: Add smart constructor for first-order algebras.

---
 src/Soat/FirstOrder/Algebra.idr | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

(limited to 'src/Soat/FirstOrder/Algebra.idr')

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
-- 
cgit v1.2.3