diff --git a/.gitignore b/.gitignore
index 0c8c123..3a19649 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,6 +13,7 @@ GPATH
 GRTAGS
 GSYMS
 GTAGS
+TAGS
 Makefile
 *.cmake
 CMakeFiles/
diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean
index e23c52e..d9bd6d5 100644
--- a/algebra/quotient_group.hlean
+++ b/algebra/quotient_group.hlean
@@ -17,6 +17,9 @@ namespace group
 
   /- Quotient Group -/
 
+  definition homotopy_of_homomorphism_eq {f g : G →g G'}(p : f = g) : f ~ g :=
+  λx : G , ap010 group_fun p x
+
   definition quotient_rel (g h : G) : Prop := N (g * h⁻¹)
 
   variable {N}
@@ -190,7 +193,7 @@ namespace group
     intro g, reflexivity
   end
 
-  definition glift_unique (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (k : quotient_group N →g G')
+  definition gelim_unique (f : G →g G') (H : Π⦃g⦄, N g → f g = 1) (k : quotient_group N →g G')
     : ( k ∘g gq_map N ~ f ) → k ~ quotient_group_elim f H :=
   begin
     intro K cg, induction cg using set_quotient.rec_prop with g,
@@ -200,7 +203,15 @@ namespace group
 
   definition gq_universal_property (f : G →g G') (H : Π⦃g⦄, N g → f g = 1)  :
     is_contr (Σ(g : quotient_group N →g G'), g ∘g gq_map N = f) :=
-  sorry
+  begin
+    fapply is_contr.mk,
+      -- give center of contraction
+    { fapply sigma.mk, exact quotient_group_elim f H, apply homomorphism_eq, exact quotient_group_compute f H },
+      -- give contraction
+    { intro pair, induction pair with g p, fapply sigma_eq, 
+      {esimp, apply homomorphism_eq, symmetry, exact gelim_unique f H g (homotopy_of_homomorphism_eq p)},
+      {fapply is_prop.elimo} }
+  end
 
     /- set generating normal subgroup -/
 
diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index 2badfa2..3ebd528 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -123,11 +123,12 @@ namespace group
     (is_normal_subgroup : is_normal R)
 
   attribute subgroup_rel.R [coercion]
-  abbreviation subgroup_to_rel      [unfold 2] := @subgroup_rel.R
-  abbreviation subgroup_has_one     [unfold 2] := @subgroup_rel.Rone
-  abbreviation subgroup_respect_mul [unfold 2] := @subgroup_rel.Rmul
-  abbreviation subgroup_respect_inv [unfold 2] := @subgroup_rel.Rinv
-  abbreviation is_normal_subgroup   [unfold 2] := @normal_subgroup_rel.is_normal_subgroup
+  abbreviation subgroup_to_rel      [parsing_only] [unfold 2] := @subgroup_rel.R
+  abbreviation subgroup_has_one     [parsing_only] [unfold 2] := @subgroup_rel.Rone
+  abbreviation subgroup_respect_mul [parsing_only] [unfold 2] := @subgroup_rel.Rmul
+  abbreviation subgroup_respect_inv [parsing_only] [unfold 2] := @subgroup_rel.Rinv
+  abbreviation is_normal_subgroup   [parsing_only] [unfold 2] :=
+  @normal_subgroup_rel.is_normal_subgroup
 
   variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
             {A B : CommGroup}
diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean
index c7cc0e3..7d6e2fc 100644
--- a/homotopy/smash.hlean
+++ b/homotopy/smash.hlean
@@ -6,9 +6,9 @@
   However, we define it (equivalently) as the pushout of the maps A + B → 2 and A + B → A × B.
 -/
 
-import homotopy.circle homotopy.join types.pointed ..move_to_lib
+import homotopy.circle homotopy.join types.pointed homotopy.cofiber ..move_to_lib
 
-open bool pointed eq equiv is_equiv sum bool prod unit circle
+open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber
 
 namespace smash
 
@@ -181,6 +181,38 @@ namespace smash
 
   /- To prove: commutative, associative -/
 
+  /- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/
+
+  definition prod_of_pwedge [unfold 3] (v : pwedge A B) : A × B :=
+  begin
+    induction v with a b ,
+    { exact (a, pt) },
+    { exact (pt, b) },
+    { reflexivity }
+  end
+
+  definition pprod_of_pwedge [constructor] : pwedge A B →* A ×* B :=
+  begin
+    fconstructor,
+    { intro v, induction v with a b ,
+      { exact (a, pt) },
+      { exact (pt, b) },
+      { reflexivity }},
+    { reflexivity }
+  end
+
+  attribute pcofiber [constructor]
+  definition pcofiber_of_smash (x : smash A B) : pcofiber (@pprod_of_pwedge A B) :=
+  begin
+    induction x,
+    { exact pushout.inr (a, b) },
+    { exact pushout.inl ⋆ },
+    { exact pushout.inl ⋆ },
+    { symmetry, },
+    { }
+  end
+
+
   /- smash A S¹ = susp A -/
   open susp
 
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 4243431..6de864b 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -7,7 +7,7 @@ open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc
 
 attribute equiv.symm equiv.trans is_equiv.is_equiv_ap fiber.equiv_postcompose
           fiber.equiv_precompose pequiv.to_pmap pequiv._trans_of_to_pmap ghomotopy_group_succ_in
-          isomorphism_of_eq pmap_bool_equiv sphere_equiv_bool psphere_pequiv_pbool fiber_eq_equiv
+          isomorphism_of_eq pmap_bool_equiv sphere_equiv_bool psphere_pequiv_pbool fiber_eq_equiv int.equiv_succ
           [constructor]
 attribute is_equiv.eq_of_fn_eq_fn' [unfold 3]
 attribute isomorphism._trans_of_to_hom [unfold 3]
@@ -25,6 +25,21 @@ open sigma
 namespace group
   open is_trunc
 
+  -- some extra instances for type class inference
+  definition is_homomorphism_comm_homomorphism [instance] {G G' : CommGroup} (φ : G →g G')
+    : @is_homomorphism G G' (@comm_group.to_group _ (CommGroup.struct G))
+                            (@comm_group.to_group _ (CommGroup.struct G')) φ :=
+  homomorphism.struct φ
+
+  definition is_homomorphism_comm_homomorphism1 [instance] {G G' : CommGroup} (φ : G →g G')
+    : @is_homomorphism G G' _
+                            (@comm_group.to_group _ (CommGroup.struct G')) φ :=
+  homomorphism.struct φ
+
+  definition is_homomorphism_comm_homomorphism2 [instance] {G G' : CommGroup} (φ : G →g G')
+    : @is_homomorphism G G' (@comm_group.to_group _ (CommGroup.struct G)) _ φ :=
+  homomorphism.struct φ
+
   theorem inv_eq_one {A : Type} [group A] {a : A} (H : a = 1) : a⁻¹ = 1 :=
   iff.mpr (inv_eq_one_iff_eq_one a) H