diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-29 14:53:03 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-29 14:53:03 +0000 |
| commit | e8d6ac1f1d9c05b71bb9098a1590e29e5c93b0b8 (patch) | |
| tree | 41913c98070f05194a15cad580aab5428dc8fa8c /src/Soat/FirstOrder/Algebra.idr | |
| parent | d6a3893ac4c77accc497b51eb47597744e1a1c84 (diff) | |
Add a bundle for raw algebra with a relation.
Diffstat (limited to 'src/Soat/FirstOrder/Algebra.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Algebra.idr | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr index 6f25f59..245af6d 100644 --- a/src/Soat/FirstOrder/Algebra.idr +++ b/src/Soat/FirstOrder/Algebra.idr @@ -27,6 +27,12 @@ MkRawAlgebra : (0 U : sig.T -> Type) -> (sem : sig `algebraOver'` U) -> RawAlgeb MkRawAlgebra u sem = MakeRawAlgebra u (\o => uncurry (sem o)) public export +record RawAlgebraWithRelation (0 sig : Signature) where + constructor MkRawAlgebraWithRelation + raw : RawAlgebra sig + 0 relation : IRel raw.U + +public export record IsAlgebra (0 sig : Signature) (0 a : RawAlgebra sig) (0 rel : IRel a.U) where constructor MkIsAlgebra equivalence : IEquivalence a.U rel @@ -45,6 +51,10 @@ public export (.setoid) a = MkISetoid a.raw.U a.relation a.algebra.equivalence public export +(.rawWithRelation) : Algebra sig -> RawAlgebraWithRelation sig +(.rawWithRelation) a = MkRawAlgebraWithRelation a.raw a.relation + +public export record IsHomomorphism {0 sig : Signature} (a, b : Algebra sig) (f : (t : sig.T) -> a.raw.U t -> b.raw.U t) |