diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-02 14:14:44 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-02 14:14:44 +0000 |
| commit | 2bd69bf893b7e1ebe4186639526451caf2083b12 (patch) | |
| tree | 9e6830a98da09c91e337b250aa0658caf4c26d69 /src/Soat/FirstOrder/Algebra.idr | |
| parent | 45e9bbec72bf338306d446012f077e195439aed0 (diff) | |
Diffstat (limited to 'src/Soat/FirstOrder/Algebra.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Algebra.idr | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr index 245af6d..26370cc 100644 --- a/src/Soat/FirstOrder/Algebra.idr +++ b/src/Soat/FirstOrder/Algebra.idr @@ -104,3 +104,11 @@ compIsHomo fHomo gHomo = MkIsHomomorphism public export compHomo : {a, b, c : Algebra sig} -> Homomorphism b c -> Homomorphism a b -> Homomorphism a c compHomo f g = MkHomomorphism _ $ compIsHomo f.homo g.homo + +public export +record Isomorphism {0 sig : Signature} (a, b : Algebra sig) where + constructor MkIsomorphism + to : Homomorphism a b + from : Homomorphism b a + fromTo : {t : sig.T} -> (x : a.raw.U t) -> a.relation t (from.func t $ to.func t x) x + toFrom : {t : sig.T} -> (x : b.raw.U t) -> b.relation t (to.func t $ from.func t x) x |