Show identity and composition are homomorphisms.

1 files changed, 33 insertions, 0 deletions

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