diff options
Diffstat (limited to 'src/Soat/FirstOrder/Algebra.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Algebra.idr | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr index 5f166d5..bbc0430 100644 --- a/src/Soat/FirstOrder/Algebra.idr +++ b/src/Soat/FirstOrder/Algebra.idr @@ -37,13 +37,13 @@ record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) w public export record Algebra (0 sig : Signature) where constructor MkAlgebra - raw : RawAlgebra sig - 0 rel : IRel raw.U - algebra : IsAlgebra sig raw rel + raw : RawAlgebra sig + 0 relation : IRel raw.U + algebra : IsAlgebra sig raw relation public export (.setoid) : Algebra sig -> ISetoid sig.T -(.setoid) a = MkISetoid a.raw.U a.rel a.algebra.equivalence +(.setoid) a = MkISetoid a.raw.U a.relation a.algebra.equivalence public export record IsHomomorphism @@ -51,9 +51,10 @@ record IsHomomorphism (f : (t : sig.T) -> a.raw.U t -> b.raw.U t) where constructor MkIsHomomorphism - cong : (t : sig.T) -> {tm, tm' : a.raw.U t} -> a.rel t tm tm' -> b.rel t (f t tm) (f t tm') + cong : (t : sig.T) -> {tm, tm' : a.raw.U t} + -> a.relation t tm tm' -> b.relation 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)) + -> b.relation t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms)) public export record Homomorphism {0 sig : Signature} (a, b : Algebra sig) |