diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:00:39 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:00:39 +0000 |
| commit | 580970d11a4e754c0c8e6f42c8312bffb1edc2db (patch) | |
| tree | 47e85bfd18a33ed6fd87e1c82181e5cdb5f6d43b /src/Soat/FirstOrder/Algebra.idr | |
| parent | 242197f40bb7957625be1e5f0bfd325af6e06be4 (diff) | |
Move IsAlgebra relation from type to body.
Diffstat (limited to 'src/Soat/FirstOrder/Algebra.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Algebra.idr | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr index f0b23ea..6f9389b 100644 --- a/src/Soat/FirstOrder/Algebra.idr +++ b/src/Soat/FirstOrder/Algebra.idr @@ -25,18 +25,22 @@ record RawSetoidAlgebra (0 sig : Signature) where 0 relation : IRel raw.U public export -record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) where +record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) where constructor MkIsAlgebra - equivalence : IEquivalence a.U rel + 0 relation : IRel a.U + equivalence : IEquivalence a.U relation 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') + -> Pointwise relation tms tms' -> relation t (a.sem op tms) (a.sem op tms') public export record Algebra (0 sig : Signature) where constructor MkAlgebra raw : RawAlgebra sig - 0 relation : IRel raw.U - algebra : IsAlgebra sig raw relation + algebra : IsAlgebra sig raw + +public export 0 +(.relation) : (0 a : Algebra sig) -> IRel a.raw.U +(.relation) a = a.algebra.relation public export (.setoid) : Algebra sig -> ISetoid sig.T |