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/FirstOrder/Algebra.idr | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'src/Soat/FirstOrder/Algebra.idr')

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