From 865e9dbdd0a7ed2b0dad75f2c672ad84e9e85bcc Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Fri, 25 Nov 2022 14:30:36 +0000 Subject: Make proofs relevant. --- 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 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 -- cgit v1.2.3