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