From a34e0b84874ff1c7f348821c65af660d1de3ece0 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 25 Nov 2022 15:37:57 +0000
Subject: Show identity and composition are homomorphisms.

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

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 5428ca3..4b40cee 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -62,3 +62,36 @@ record Homomorphism {0 sig : Signature} (a, b : Algebra sig)
   constructor MkHomomorphism
   func : IFunc a.raw.U b.raw.U
   homo : IsHomomorphism a b func
+
+public export
+idIsHomo : {a : Algebra sig} -> IsHomomorphism a a (\_ => Basics.id)
+idIsHomo = MkIsHomomorphism
+  (\_ => id)
+  (\op, tms =>
+    (a.algebra.equivalence _).equalImpliesEq $
+    sym $
+    cong (a.raw.sem op) $
+    mapId tms)
+
+public export
+idHomo : {a : Algebra sig} -> Homomorphism a a
+idHomo = MkHomomorphism _ idIsHomo
+
+public export
+compIsHomo : {a, b, c : Algebra sig} -> {f : IFunc b.raw.U c.raw.U} -> {g : IFunc a.raw.U b.raw.U}
+  -> IsHomomorphism b c f -> IsHomomorphism a b g -> IsHomomorphism a c (\i => f i . g i)
+compIsHomo fHomo gHomo = MkIsHomomorphism
+  (\t => fHomo.cong t . gHomo.cong t)
+  (\op, tms =>
+    (c.algebra.equivalence _).transitive
+      (fHomo.cong _ $ gHomo.semHomo op tms) $
+    (c.algebra.equivalence _).transitive
+      (fHomo.semHomo op (map g tms)) $
+    (c.algebra.equivalence _).equalImpliesEq $
+    sym $
+    cong (c.raw.sem op) $
+    mapComp tms)
+
+public export
+compHomo : {a, b, c : Algebra sig} -> Homomorphism b c -> Homomorphism a b -> Homomorphism a c
+compHomo f g = MkHomomorphism _ $ compIsHomo f.homo g.homo
-- 
cgit v1.2.3