diff --git a/examples/algebra.pg b/examples/algebra.pg
index 0c47785..a2785a7 100644
--- a/examples/algebra.pg
+++ b/examples/algebra.pg
@@ -2,69 +2,87 @@
 
 section Magma
 
-variable (G : ★);
-def binop := G → G → G;
+variable (G H : ★);
+def binop (A : ★) := A → A → A;
 
 def = := eq G;
 infixl 1 =;
 
-variable (* : binop);
+def ~ := eq H;
+infixl 1 ~;
+
+variable (* : binop G);
 infixl 20 *;
 
+variable (+ : binop H);
+infixl 20 +;
+
+variable (f : G → H);
+hypothesis (f_homo : forall (a b : G), f (a * b) ~ f a * f b);
+
 def *> (a b : G) := b * a;
 infixl 20 *>;
 
 section Semigroup
 
-def assoc := forall (a b c : G), a * (b * c) = a * b * c;
-hypothesis (Hassoc : assoc);
+hypothesis (assocG : forall (a b c : G), a * (b * c) = a * b * c);
+hypothesis (assocH : forall (a b c : H), a + (b + c) ~ a + b + c);
 
 def assoc_op (a b c : G) : a *> (b *> c) = a *> b *> c := 
-    eq_sym G (a *> b *> c) (a *> (b *> c)) (Hassoc c b a);
+    eq_sym G (a *> b *> c) (a *> (b *> c)) (assocG c b a);
 
 section Monoid
 
 variable (e : G);
-def id_l := forall (a : G), e * a = a;
-def id_r := forall (a : G), a * e = a;
+variable (eH : H);
 
-hypothesis (Hid_l : id_l);
-hypothesis (Hid_r : id_r);
+hypothesis (id_lG : forall (a : G), e * a = a);
+hypothesis (id_rG : forall (a : G), a * e = a);
 
-def id_l_op : forall (a : G), e *> a = a := Hid_r;
-def id_r_op : forall (a : G), a *> e = a := Hid_l;
+hypothesis (id_lH : forall (a : H), e * a = a);
+hypothesis (id_rH : forall (a : H), a * e = a);
 
-def left_id_unique (a : G) : #id_l G (*) a → a = e :=
-    fun (H : #id_l G (*) a) =>
-        eq_trans G a (a * e) e
-            (eq_sym G (a * e) a (Hid_r a))
-            (H e);
+def id_l_op : forall (a : G), e *> a = a := id_rG;
+def id_r_op : forall (a : G), a *> e = a := id_lG;
 
-def right_id_unique (a : G) : #id_r G (*) a → a = e := #left_id_unique G (*>) e Hid_l a;
+def left_id_unique (a : G) (H : forall (b : G), a * b = b) : a = e :=
+    eq_trans G a (a * e) e (eq_sym G (a * e) a (id_rG a)) (H e);
+
+def right_id_unique (a : G) (H : forall (b : G), b * a = b) : a = e := #left_id_unique G (*>) e id_lG a H;
 
 section Group
 
 variable (i : G → G);
-hypothesis (Hinv_l : forall (a : G), i a * a = e);
-hypothesis (Hinv_r : forall (a : G), a * i a = e);
+hypothesis (inv_lG : forall (a : G), i a * a = e);
+hypothesis (inv_rG : forall (a : G), a * i a = e);
+
+variable (j : H → H);
+hypothesis (inv_lH : forall (a : H), j a * a ~ eH);
+hypothesis (inv_rH : forall (a : H), a * j a ~ eH);
 
 def left_inv_unique (a b : G) (h : b * a = e) : b = i a :=
     eq_trans G b (b * e) (i a)
-        (eq_sym G (b * e) b (Hid_r b))
+        (eq_sym G (b * e) b (id_rG b))
         (eq_trans G (b * e) (b * (a * i a)) (i a)
             (eq_cong G G e (a * i a) ((*) b)
-                (eq_sym G (a * i a) e (Hinv_r a)))
+                (eq_sym G (a * i a) e (inv_rG a)))
             (eq_trans G (b * (a * i a)) (b * a * i a) (i a)
-                (Hassoc b a (i a))
+                (assocG b a (i a))
                 (eq_trans G (b * a * i a) (e * i a) (i a)
                     (eq_cong G G (b * a) e ([z : G] z * i a) h)
-                    (Hid_l (i a)))));
+                    (id_lG (i a)))));
 
 def right_inv_unique (a b : G) (h : a * b = e) : b = i a :=
-    #left_inv_unique G (*>) assoc_op e Hid_r Hid_l i Hinv_l a b h;
+    #left_inv_unique G (*>) assoc_op e id_rG id_lG i inv_lG a b h;
+
+def homo_preserve_inv (a : G) : f (i a) ~ j (f a) :=
+    #left_inv_unique H (+) assocH eH id_lH id_rH j inv_rH (f a) (f (i a))
+    (eq_trans H (f a * f (i a)) (f (a * i a)) 
+    )
+        -- WTS: f a * f (i a) ~ eH
 
 def inverse_involutive (a : G) : i (i a) = a :=
-    eq_sym G a (i (i a)) (right_inv_unique (i a) a (Hinv_l a));
+    eq_sym G a (i (i a)) (right_inv_unique (i a) a (inv_lG a));
 
 def shoes_and_socks (a b : G) : i (a * b) = i b * i a :=
     eq_sym G (i b * i a) (i (a * b))
@@ -73,34 +91,34 @@ def shoes_and_socks (a b : G) : i (a * b) = i b * i a :=
         (under_ai (x y : G) (h : x = y) := eq_cong G G x y ([z : G] z * (i a)) h)
      in
         eq_trans G (a * b * (i b * i a)) (a * b * i b * i a) e
-        (Hassoc (a * b) (i b) (i a))
+        (assocG (a * b) (i b) (i a))
         (eq_trans G (a * b * i b * i a) (a * (b * i b) * i a) e
-            (under_ai (a * b * i b) (a * (b * i b)) (eq_sym G (a * (b * i b)) (a * b * i b) (Hassoc a b (i b))))
+            (under_ai (a * b * i b) (a * (b * i b)) (eq_sym G (a * (b * i b)) (a * b * i b) (assocG a b (i b))))
             (eq_trans G (a * (b * i b) * i a) (a * e * i a) e
-                (eq_cong G G (b * i b) e (fun (x : G) => (a * x * i a)) (Hinv_r b))
+                (eq_cong G G (b * i b) e (fun (x : G) => (a * x * i a)) (inv_rG b))
                 (eq_trans G (a * e * i a) (a * i a) e
-                    (under_ai (a * e) a (Hid_r a))
-                    (Hinv_r a))))
+                    (under_ai (a * e) a (id_rG a))
+                    (inv_rG a))))
      end));
 
 def cancel_l (a b c : G) (h : a * b = a * c) : b = c :=
     eq_trans G b (e * b) c
-        (eq_sym G (e * b) b (Hid_l b))
+        (eq_sym G (e * b) b (id_lG b))
         (eq_trans G (e * b) (i a * a * b) c
             (eq_cong G G e (i a * a) ([x : G] x * b)
-                (eq_sym G (i a * a) e (Hinv_l a)))
+                (eq_sym G (i a * a) e (inv_lG a)))
             (eq_trans G (i a * a * b) (i a * (a * b)) c
-                (eq_sym G (i a * (a * b)) (i a * a * b) (Hassoc (i a) a b))
+                (eq_sym G (i a * (a * b)) (i a * a * b) (assocG (i a) a b))
                 (eq_trans G (i a * (a * b)) (i a * (a * c)) c
                     (eq_cong G G (a * b) (a * c) ((*) (i a)) h)
                     (eq_trans G (i a * (a * c)) (i a * a * c) c
-                        (Hassoc (i a) a c)
+                        (assocG (i a) a c)
                         (eq_trans G (i a * a * c) (e * c) c
-                            (eq_cong G G (i a * a) e ([x : G] x * c) (Hinv_l a))
-                            (Hid_l c))))));
+                            (eq_cong G G (i a * a) e ([x : G] x * c) (inv_lG a))
+                            (id_lG c))))));
 
 def cancel_r (a b c : G) (h : b * a = c * a) : b = c :=
-    #cancel_l G (*>) assoc_op e Hid_r i Hinv_r a b c h;
+    #cancel_l G (*>) assoc_op e id_rG i inv_rG a b c h;
 
 def abelian : ★ := forall (a b : G), a * b = b * a;
 
@@ -108,16 +126,16 @@ def left_right_cancel : (forall (x y z : G), x * y = z * x → y = z) → abelia
     fun (h : forall (x y z : G), x * y = z * x → y = z) (a b : G) =>
         h (i a) (a * b) (b * a)
         (eq_trans G (i a * (a * b)) (i a * a * b) (b * a * i a)
-            (Hassoc (i a) a b)
+            (assocG (i a) a b)
             (eq_trans G (i a * a * b) (e * b) (b * a * i a)
-                (eq_cong G G (i a * a) e ([x : G] x * b) (Hinv_l a))
+                (eq_cong G G (i a * a) e ([x : G] x * b) (inv_lG a))
                 (eq_trans G (e * b) b (b * a * i a)
-                    (Hid_l b)
+                    (id_lG b)
                     (eq_trans G b (b * e) (b * a * i a)
-                        (eq_sym G (b * e) b (Hid_r b))
+                        (eq_sym G (b * e) b (id_rG b))
                         (eq_trans G (b * e) (b * (a * i a)) (b * a * i a)
-                            (eq_cong G G e (a * i a) ((*) b) (eq_sym G (a * i a) e (Hinv_r a)))
-                            (Hassoc b a (i a)))))));
+                            (eq_cong G G e (a * i a) ((*) b) (eq_sym G (a * i a) e (inv_rG a)))
+                            (assocG b a (i a)))))));
 
 def inv_distrib_abelian : (forall (a b : G), i (a * b) = i a * i b) → abelian :=
     fun (h : forall (a b : G), i (a * b) = i a * i b) (a b : G) =>