Inline definition of IsHomomorphism.

1 files changed, 21 insertions, 34 deletions

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index b9c02c5..7bed448 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -53,52 +53,39 @@ public export
 (.rawSetoid) a = MkRawSetoidAlgebra a.raw a.relation
 
 public export
-record IsHomomorphism
-  {0 sig : Signature} (a, b : Algebra sig)
-  (f : (t : sig.T) -> a.raw.U t -> b.raw.U t)
-  where
-  constructor MkIsHomomorphism
-  cong    : (t : sig.T) -> {tm, tm' : a.raw.U t}
-    -> a.relation t tm tm' -> b.relation t (f t tm) (f t tm')
-  semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
-    -> b.relation t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms))
-
-public export
 record (~>) {0 sig : Signature} (a, b : Algebra sig)
   where
   constructor MkHomomorphism
-  func : IFunc a.raw.U b.raw.U
-  homo : IsHomomorphism a b func
+  func    : (t : sig.T) -> a.raw.U t -> b.raw.U t
+  cong    : (t : sig.T) -> {tm, tm' : a.raw.U t}
+    -> a.relation t tm tm' -> b.relation t (func t tm) (func t tm')
+  semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
+    -> b.relation t (func t (a.raw.sem op tms)) (b.raw.sem op (map func tms))
 
 public export
-idIsHomo : {a : Algebra sig} -> IsHomomorphism a a (\_ => Basics.id)
-idIsHomo = MkIsHomomorphism
-  (\_ => id)
-  (\op, tms =>
+idHomo : {a : Algebra sig} -> a ~> a
+idHomo = MkHomomorphism
+  { func    = \_ => id
+  , cong    = \_ => id
+  , semHomo = \op, tms =>
     (a.algebra.equivalence _).equalImpliesEq $
     sym $
     cong (a.raw.sem op) $
-    mapId tms)
+    mapId tms
+  }
 
 public export
-idHomo : {a : Algebra sig} -> 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 =>
+compHomo : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
+compHomo f g = MkHomomorphism
+  { func    = \t => f.func t . g.func t
+  , cong    = \t => f.cong t . g.cong t
+  , semHomo = \op, tms =>
     (c.algebra.equivalence _).transitive
-      (fHomo.cong _ $ gHomo.semHomo op tms) $
+      (f.cong _ $ g.semHomo op tms) $
     (c.algebra.equivalence _).transitive
-      (fHomo.semHomo op (map g tms)) $
+      (f.semHomo op (map g.func tms)) $
     (c.algebra.equivalence _).equalImpliesEq $
     sym $
     cong (c.raw.sem op) $
-    mapComp tms)
-
-public export
-compHomo : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
-compHomo f g = MkHomomorphism _ $ compIsHomo f.homo g.homo
+    mapComp tms
+  }