From 332f481a61429c031016fd5d43238095d1a22075 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 5 Dec 2022 15:55:09 +0000 Subject: refactor : rename homomorphism combinators. - idHomo -> id - compHomo -> (.) --- src/Soat/FirstOrder/Algebra.idr | 8 ++++---- src/Soat/FirstOrder/Algebra/Coproduct.idr | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) (limited to 'src/Soat/FirstOrder') 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 -- cgit v1.2.3