From 1fcb41a4e7aa2997ff03f519bfa040c77b8afabb Mon Sep 17 00:00:00 2001
From: Steve Awodey <sawodey@gmail.com>
Date: Thu, 10 Nov 2016 15:40:30 -0500
Subject: [PATCH] wip

quotient homomorphism
---
 algebra/.#exact_couple.hlean |  1 +
 algebra/quotient_group.hlean | 11 +++++++++++
 2 files changed, 12 insertions(+)
 create mode 120000 algebra/.#exact_couple.hlean

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