diff options
Diffstat (limited to 'src/Soat/FirstOrder/Algebra.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Algebra.idr | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr index fef5871..5f166d5 100644 --- a/src/Soat/FirstOrder/Algebra.idr +++ b/src/Soat/FirstOrder/Algebra.idr @@ -30,8 +30,8 @@ MkRawAlgebra u sem = MakeRawAlgebra u (\o => uncurry (sem o)) public export record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) where constructor MkIsAlgebra - 0 equivalence : IEquivalence a.U rel - 0 semCong : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity} + equivalence : IEquivalence a.U rel + semCong : {t : sig.T} -> (op : Op sig t) -> {tms, tms' : a.U ^ op.arity} -> Pointwise rel tms tms' -> rel t (a.sem op tms) (a.sem op tms') public export @@ -51,8 +51,8 @@ record IsHomomorphism (f : (t : sig.T) -> a.raw.U t -> b.raw.U t) where constructor MkIsHomomorphism - 0 cong : (t : sig.T) -> {tm, tm' : a.raw.U t} -> a.rel t tm tm' -> b.rel t (f t tm) (f t tm') - 0 semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity) + cong : (t : sig.T) -> {tm, tm' : a.raw.U t} -> a.rel t tm tm' -> b.rel t (f t tm) (f t tm') + semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity) -> b.rel t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms)) public export |