diff --git a/algebra/.#exact_couple.hlean b/algebra/.#exact_couple.hlean
new file mode 120000
index 0000000..c4be726
--- /dev/null
+++ b/algebra/.#exact_couple.hlean
@@ -0,0 +1 @@
+Steve@steveawodeysAir.wv.cc.cmu.edu.255
\ No newline at end of file
diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean
index 9f9caba..52da343 100644
--- a/algebra/quotient_group.hlean
+++ b/algebra/quotient_group.hlean
@@ -220,6 +220,17 @@ namespace group
       {fapply is_prop.elimo} }
   end
 
+definition comm_group_quotient_homomorphism (A B : CommGroup)(K : subgroup_rel A)(L : subgroup_rel B) (f : A →g B)
+     (p : Π(a:A), K(a) → L(f a)) : quotient_comm_group K →g quotient_comm_group L :=
+    begin
+    fapply quotient_group_elim,
+    exact (comm_gq_map L) ∘g f,
+    
+-- homomorphism.mk,
+  
+
+    end
+
     /- set generating normal subgroup -/
 
   section