diff options
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 |