diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 15:40:44 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 15:40:44 +0000 |
| commit | bfac93dbe8c98d193feb165a088c6a7c79382d27 (patch) | |
| tree | d45269488c81ac07a27927d0a0cd2856250adfdd | |
| parent | 57a299ee52f29aa553a9d93c24f4c1e9eee4fa27 (diff) | |
Provide more bundles from algebras.
| -rw-r--r-- | src/Soat/SecondOrder/Algebra.idr | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr index 5457385..9f9719e 100644 --- a/src/Soat/SecondOrder/Algebra.idr +++ b/src/Soat/SecondOrder/Algebra.idr @@ -112,6 +112,19 @@ public export (.setoid) a = MkISetoid (uncurry a.raw.U) a.relation a.algebra.equivalence public export +(.setoidAt) : Algebra sig -> (ctx : List sig.T) -> ISetoid sig.T +(.setoidAt) a ctx = MkISetoid + (flip a.raw.U ctx) + (\t => a.relation (t, ctx)) + (\_ => a.algebra.equivalence _) + +public export +(.varFunc) : (a : Algebra sig) -> (ctx : _) -> IFunction (isetoid (flip Elem ctx)) (a.setoidAt ctx) +(.varFunc) a ctx = MkIFunction + (\_ => a.raw.var) + (\_ => (a.algebra.equivalence _).equalImpliesEq . cong a.raw.var) + +public export record IsHomomorphism {0 sig : Signature} (a, b : Algebra sig) (f : (t : sig.T) -> (ctx : List sig.T) -> a.raw.U t ctx -> b.raw.U t ctx) |