From 332f481a61429c031016fd5d43238095d1a22075 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 5 Dec 2022 15:55:09 +0000
Subject: refactor : rename homomorphism combinators.

- idHomo -> id
- compHomo -> (.)
---
 src/Soat/SecondOrder/Algebra/Lift.idr | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'src/Soat/SecondOrder/Algebra')

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
-- 
cgit v1.2.3