diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 14:30:36 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 14:30:36 +0000 |
| commit | 865e9dbdd0a7ed2b0dad75f2c672ad84e9e85bcc (patch) | |
| tree | 72488a96f195321a26c5248a156941ed9ce42fe6 /src/Soat/FirstOrder/Algebra.idr | |
| parent | 7c8591b566baeb6af42a22b8979c53ebdcab5479 (diff) | |
Make proofs relevant.
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 |