refactor : rename homomorphism combinators.

- idHomo -> id
- compHomo -> (.)

3 files changed, 18 insertions, 18 deletions

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index 7bed448..6e39612 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -63,8 +63,8 @@ record (~>) {0 sig : Signature} (a, b : Algebra sig)
     -> b.relation t (func t (a.raw.sem op tms)) (b.raw.sem op (map func tms))
 
 public export
-idHomo : {a : Algebra sig} -> a ~> a
-idHomo = MkHomomorphism
+id : {a : Algebra sig} -> a ~> a
+id = MkHomomorphism
   { func    = \_ => id
   , cong    = \_ => id
   , semHomo = \op, tms =>
@@ -75,8 +75,8 @@ idHomo = MkHomomorphism
   }
 
 public export
-compHomo : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
-compHomo f g = MkHomomorphism
+(.) : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
+(.) f g = MkHomomorphism
   { func    = \t => f.func t . g.func t
   , cong    = \t => f.cong t . g.cong t
   , semHomo = \op, tms =>
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index a98391b..5cb4c45 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -195,8 +195,8 @@ coproductUnique' : {x, y, z : Algebra sig}
   -> z.relation t (f.func t tm) (g.func t tm)
 coproductUnique' f g congL congR tm = bindUnique'
   { v = fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))
-  , f = compHomo f $ termToCoproduct x y
-  , g = compHomo g $ termToCoproduct x y
+  , f = f . termToCoproduct x y
+  , g = g . termToCoproduct x y
   , cong = \x => case x of
       (Left x) => congL x
       (Right x) => congR x
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index 9a88446..596bb24 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -141,14 +141,14 @@ InitialIsAlgebra sig = MkIsAlgebra
     eq)
   (\t, ctx, tm =>
     tmRelSym (\_ => MkSymmetric symmetric) $
-    bindUnique (renameBodyFunc reflexive) idHomo (\i => Done' $ sym $ curryUncurry id i) $
+    bindUnique (renameBodyFunc reflexive) id (\i => Done' $ sym $ curryUncurry id i) $
     tm)
   (\t, f, g, tm =>
     tmRelSym (\_ => MkSymmetric symmetric) $
     bindUnique
       {a = FreeAlgebra (isetoid (flip Elem _))}
       (renameBodyFunc (transitive g f))
-      (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (renameBodyFunc g)))
+      (bindHomo (renameBodyFunc f) . bindHomo (renameBodyFunc g))
       (\i => Done' $ sym $ curryUncurry (curry f . curry g) i) $
     tm)
   (\f, (MkOp (Op op)), tms =>
@@ -172,7 +172,7 @@ InitialIsAlgebra sig = MkIsAlgebra
     bindUnique
       {a = FreeAlgebra (isetoid (flip Elem _))}
       (indexFunc _)
-      (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (indexFunc tms)))
+      (bindHomo (renameBodyFunc f) . bindHomo (indexFunc tms))
       (\i =>
         tmRelReflexive (\_ => MkReflexive reflexive) $
         sym $
@@ -182,7 +182,7 @@ InitialIsAlgebra sig = MkIsAlgebra
     bindUnique
       {a = FreeAlgebra (isetoid (flip Elem _))}
       (indexFunc _)
-      (compHomo (bindHomo (indexFunc tms)) (bindHomo (renameBodyFunc f)))
+      (bindHomo (indexFunc tms) . bindHomo (renameBodyFunc f))
       (\i =>
         tmRelReflexive (\_ => MkReflexive reflexive) $
         sym $
@@ -192,7 +192,7 @@ InitialIsAlgebra sig = MkIsAlgebra
     bindUnique
       {a = FreeAlgebra (isetoid (flip Elem _))}
       (indexFunc _)
-      (compHomo (bindHomo (indexFunc tms')) (bindHomo (indexFunc tms)))
+      (bindHomo (indexFunc tms') . bindHomo (indexFunc tms))
       (\i =>
         tmRelReflexive (\_ => MkReflexive reflexive) $
         sym $
@@ -204,7 +204,7 @@ InitialIsAlgebra sig = MkIsAlgebra
     bindUnique
       {a = FreeAlgebra (isetoid (flip Elem _))}
       (indexFunc _)
-      idHomo
+      id
       (\i =>
         tmRelReflexive (\_ => MkReflexive reflexive) $
         sym $
@@ -229,7 +229,7 @@ InitialIsAlgebra sig = MkIsAlgebra
             (bindUnique
                {a = FreeAlgebra (isetoid (flip Elem _))}
                (renameBodyFunc _)
-               idHomo
+               id
                (\i =>
                  Done' $
                  sym $
@@ -269,8 +269,8 @@ fromInitialHomo a = MkHomomorphism
   (\t, f => bindUnique'
     {v = isetoid (flip Elem _)}
     {a = projectAlgebra sig a _}
-    (compHomo (bindHomo (a.varFunc _)) (bindHomo (renameBodyFunc f)))
-    (compHomo (a.renameHomo f) (bindHomo (a.varFunc _)))
+    (bindHomo (a.varFunc _) . bindHomo (renameBodyFunc f))
+    (a.renameHomo f . bindHomo (a.varFunc _))
     (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i))
   (\ctx, (MkOp (Op op)), tms =>
     a.algebra.semCong ctx (MkOp (Op op)) $
@@ -286,8 +286,8 @@ fromInitialHomo a = MkHomomorphism
   (\t, ctx, tm, tms => bindUnique'
     {v = isetoid (flip Elem _)}
     {a = projectAlgebra sig a _}
-    (compHomo (bindHomo (a.varFunc _)) (bindHomo (indexFunc tms)))
-    (compHomo (a.substHomo1 ctx _) (bindHomo (a.varFunc _)))
+    (bindHomo (a.varFunc _) . bindHomo (indexFunc tms))
+    (a.substHomo1 ctx _ . bindHomo (a.varFunc _))
     (\i =>
       (a.algebra.equivalence _).transitive
         (bindUnique
@@ -313,5 +313,5 @@ fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique
   {v = isetoid (flip Elem _)}
   {a = projectAlgebra sig a ctx}
   (a.varFunc ctx)
-  (compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx))
+  (projectHomo f ctx . freeToInitialHomo sig ctx)
   f.varHomo