From 2bd69bf893b7e1ebe4186639526451caf2083b12 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 2 Dec 2022 14:14:44 +0000
Subject: WIP: Frex is free

---
 src/Soat/FirstOrder/Algebra.idr | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/Soat/FirstOrder/Algebra.idr')

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
-- 
cgit v1.2.3