From 83c85bf396949287365a694a89e0f49a58cab5a2 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 6 Dec 2022 15:33:27 +0000
Subject: Cast algebraic structure as setoid homomorphisms.

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

(limited to 'src/Soat/FirstOrder')

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 97b6adc..982e54e 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -54,6 +54,11 @@ public export
 (.rawSetoid) : Algebra sig -> RawSetoidAlgebra sig
 (.rawSetoid) a = MkRawSetoidAlgebra a.raw a.relation
 
+public export
+(.semFunc) : (a : Algebra sig) -> {t : sig.T} -> (op : Op sig t)
+  -> index (Product a.setoid) op.arity ~> index a.setoid t
+a .semFunc op = MkSetoidHomomorphism (a.raw.sem op) (\_, _ => a.algebra.semCong op)
+
 public export
 record (~>) {0 sig : Signature} (a, b : Algebra sig)
   where
-- 
cgit v1.2.3