diff options
Diffstat (limited to 'src/Soat/FirstOrder')
| -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) |