diff options
| -rw-r--r-- | src/Soat/FirstOrder/Algebra.idr | 8 | ||||
| -rw-r--r-- | src/Soat/FirstOrder/Algebra/Coproduct.idr | 4 | ||||
| -rw-r--r-- | src/Soat/SecondOrder/Algebra/Lift.idr | 24 |
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 |