Inline definition of IsHomomorphism.

1 files changed, 10 insertions, 18 deletions

diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr
index 0ab235b..d3e1f4c 100644
--- a/src/Soat/SecondOrder/Algebra.idr
+++ b/src/Soat/SecondOrder/Algebra.idr
@@ -132,31 +132,23 @@ public export
   (\_ => (a.algebra.equivalence _).equalImpliesEq . cong a.raw.var)
 
 public export
-record IsHomomorphism
-  {0 sig : Signature} (a, b : Algebra sig)
-  (f : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx)
+record (~>) {0 sig : Signature} (a, b : Algebra sig)
   where
-  constructor MkIsHomomorphism
+  constructor MkHomomorphism
+  func       : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx
   cong       : (t : sig.T) -> (ctx : List sig.T) -> {tm, tm' : a.raw.U t ctx}
-    -> a.relation (t, ctx) tm tm' -> b.relation (t, ctx) (f t ctx tm) (f t ctx tm')
+    -> a.relation (t, ctx) tm tm' -> b.relation (t, ctx) (func t ctx tm) (func t ctx tm')
   renameHomo : (t : sig.T) -> {ctx, ctx' : _} -> (g : ctx `Sublist` ctx') -> (tm : a.raw.U t ctx)
-    -> b.relation (t, ctx') (f t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ f t ctx tm)
+    -> b.relation (t, ctx') (func t ctx' $ a.raw.rename t g tm) (b.raw.rename t g $ func t ctx tm)
   semHomo    : (ctx : List sig.T) -> {t : sig.T} -> (op : Op sig t)
     -> (tms : extend a.raw.U ctx ^ op.arity)
     -> b.relation (t, ctx)
-         (f t ctx $ a.raw.sem ctx op tms)
-         (b.raw.sem ctx op $ map (\ty => f (snd ty) (fst ty ++ ctx)) tms)
+         (func t ctx $ a.raw.sem ctx op tms)
+         (b.raw.sem ctx op $ map (\ty => func (snd ty) (fst ty ++ ctx)) tms)
   varHomo    : {t : _} -> {ctx : _} -> (i : Elem t ctx)
-    -> b.relation (t, ctx) (f t ctx $ a.raw.var i) (b.raw.var i)
+    -> b.relation (t, ctx) (func t ctx $ a.raw.var i) (b.raw.var i)
   substHomo  : (t : sig.T) -> (ctx : List sig.T) -> {ctx' : _} -> (tm : a.raw.U t ctx')
     -> (tms : (\t => a.raw.U t ctx) ^ ctx')
     -> b.relation (t, ctx)
-         (f t ctx $ a.raw.subst t ctx tm tms)
-         (b.raw.subst t ctx (f t ctx' tm) $ map (\t => f t ctx) tms)
-
-public export
-record (~>) {0 sig : Signature} (a, b : Algebra sig)
-  where
-  constructor MkHomomorphism
-  func : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx
-  homo : IsHomomorphism a b func
+         (func t ctx $ a.raw.subst t ctx tm tms)
+         (b.raw.subst t ctx (func t ctx' tm) $ map (\t => func t ctx) tms)