diff --git a/algebra/group_constructions.hlean b/algebra/group_constructions.hlean
index fb233ac..4485f17 100644
--- a/algebra/group_constructions.hlean
+++ b/algebra/group_constructions.hlean
@@ -220,7 +220,7 @@ namespace group
     is_contr (Σ(g : quotient_group N →g G'), g ∘g gq_map N = f) :=
   sorry
 
-  /- Binary products (direct sums) of Groups -/
+  /- Binary products (direct product) of Groups -/
   definition product_one [constructor] : G × G' := (one, one)
   definition product_inv [unfold 3] : G × G' → G × G' :=
   λv, (v.1⁻¹, v.2⁻¹)
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index fce26d2..43f7ff8 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -6,14 +6,17 @@ Authors: Michael Shulman, Floris van Doorn
 -/
 
 import types.int types.pointed types.trunc homotopy.susp algebra.homotopy_group homotopy.chain_complex cubical .splice homotopy.LES_of_homotopy_groups
-open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi
+open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
 
 /-----------------------------------------
   Stuff that should go in other files
 -----------------------------------------/
 
-attribute equiv.symm equiv.trans is_equiv.is_equiv_ap fiber.equiv_postcompose fiber.equiv_precompose pequiv.to_pmap pequiv._trans_of_to_pmap [constructor]
+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 [constructor]
 attribute is_equiv.eq_of_fn_eq_fn' [unfold 3]
+attribute isomorphism._trans_of_to_hom [unfold 3]
+attribute homomorphism.struct [unfold 3]
+attribute pequiv.trans pequiv.symm [constructor]
 
 namespace sigma
 
@@ -26,6 +29,25 @@ open sigma
 namespace group
   open is_trunc
   definition pSet_of_Group (G : Group) : Set* := ptrunctype.mk G _ 1
+
+  definition pmap_of_isomorphism [constructor] {G₁ G₂ : Group} (φ : G₁ ≃g G₂) :
+    pType_of_Group G₁ →* pType_of_Group G₂ :=
+  pequiv_of_isomorphism φ
+
+  definition pequiv_of_isomorphism_of_eq {G₁ G₂ : Group} (p : G₁ = G₂) :
+    pequiv_of_isomorphism (isomorphism_of_eq p) = pequiv_of_eq (ap pType_of_Group p) :=
+  begin
+    induction p,
+    apply pequiv_eq,
+    fapply pmap_eq,
+    { intro g, reflexivity},
+    { apply is_prop.elim}
+  end
+
+  definition homomorphism_change_fun [constructor] {G₁ G₂ : Group} (φ : G₁ →g G₂) (f : G₁ → G₂)
+    (p : φ ~ f) : G₁ →g G₂ :=
+  homomorphism.mk f (λg h, (p (g * h))⁻¹ ⬝ to_respect_mul φ g h ⬝ ap011 mul (p g) (p h))
+
 end group open group
 
 namespace eq
@@ -170,6 +192,16 @@ namespace pointed
     pequiv_of_equiv (pi_equiv_pi_right g)
       begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end
 
+  definition pcast_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a)
+    {a₁ a₂ : A} (p : a₁ = a₂) : pcast (ap C p) ∘* f a₁ ~* f a₂ ∘* pcast (ap B p) :=
+  phomotopy.mk
+    begin induction p, reflexivity end
+    begin induction p, esimp, refine !idp_con ⬝ !idp_con ⬝ !ap_id⁻¹ end
+
+  definition pequiv_of_eq_commute [constructor] {A : Type} {B C : A → Type*} (f : Πa, B a →* C a)
+    {a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) :=
+  pcast_commute f p
+
 end pointed
 open pointed
 
@@ -399,19 +431,42 @@ namespace spectrum
       intro n, exact sorry
     end
 
-   definition π_glue (X : spectrum) (n : ℤ) : π*[2] (X (2 - succ n)) ≃* π*[3] (X (2 - n)) :=
+  definition π_glue (X : spectrum) (n : ℤ) : π*[2] (X (2 - succ n)) ≃* π*[3] (X (2 - n)) :=
   begin
-    symmetry,
-    refine pequiv_of_eq (phomotopy_group_succ_in (X (2 - n)) 2) ⬝e* _,
-    assert H : 2 - n = succ (2 - succ n), exact (sub_add_cancel (2-n) 1)⁻¹ ⬝ ap succ !sub_sub,
-    refine phomotopy_group_pequiv 2 (loop_pequiv_loop (pequiv_of_eq (ap X H))) ⬝e* _,
-    exact phomotopy_group_pequiv 2 (equiv_glue X (2 - succ n))⁻¹ᵉ*
+    refine phomotopy_group_pequiv 2 (equiv_glue X (2 - succ n)) ⬝e* _,
+    assert H : succ (2 - succ n) = 2 - n, exact ap succ !sub_sub⁻¹ ⬝ sub_add_cancel (2-n) 1,
+    exact pequiv_of_eq (ap (λn, π*[2] (Ω (X n))) H),
+  end
+
+  definition πg_glue (X : spectrum) (n : ℤ) : πg[1+1] (X (2 - succ n)) ≃g πg[2+1] (X (2 - n)) :=
+  begin
+    refine homotopy_group_isomorphism_of_pequiv 1 (equiv_glue X (2 - succ n)) ⬝g _,
+    assert H : succ (2 - succ n) = 2 - n, exact ap succ !sub_sub⁻¹ ⬝ sub_add_cancel (2-n) 1,
+    exact isomorphism_of_eq (ap (λn, πg[1+1] (Ω (X n))) H),
+  end
+
+  definition πg_glue_homotopy_π_glue (X : spectrum) (n : ℤ) : πg_glue X n ~ π_glue X n :=
+  begin
+    intro x,
+    esimp [πg_glue, π_glue],
+    apply ap (λp, cast p _),
+    refine !ap_compose'⁻¹ ⬝ !ap_compose'
   end
 
-  /- TODO: fill in sorry -/
   definition π_glue_square {X Y : spectrum} (f : X →ₛ Y) (n : ℤ) :
     π_glue Y n ∘* π→*[2] (f (2 - succ n)) ~* π→*[3] (f (2 - n)) ∘* π_glue X n :=
-  sorry
+  begin
+    refine !passoc ⬝* _,
+    assert H1 : phomotopy_group_pequiv 2 (equiv_glue Y (2 - succ n)) ∘* π→*[2] (f (2 - succ n))
+     ~* π→*[2] (Ω→ (f (succ (2 - succ n)))) ∘* phomotopy_group_pequiv 2 (equiv_glue X (2 - succ n)),
+    { refine !phomotopy_group_functor_compose⁻¹* ⬝* _,
+      refine phomotopy_group_functor_phomotopy 2 !sglue_square ⬝* _,
+      apply phomotopy_group_functor_compose },
+    refine pwhisker_left _ H1 ⬝* _, clear H1,
+    refine !passoc⁻¹* ⬝* _ ⬝* !passoc,
+    apply pwhisker_right,
+    refine !pequiv_of_eq_commute ⬝* by reflexivity
+  end
 
   section
   open chain_complex prod fin group
@@ -441,8 +496,10 @@ namespace spectrum
   definition is_homomorphism_LES_of_shomotopy_groups :
     Π(v : +3ℤ), is_homomorphism (cc_to_fn LES_of_shomotopy_groups v)
   | (n, fin.mk 0 H) := proof homomorphism.struct (πₛ→[n] f) qed
-  | (n, fin.mk 1 H) := proof homomorphism.struct (πₛ→[n] (spoint f))  qed
-  | (n, fin.mk 2 H) := proof is_homomorphism_compose sorry sorry qed
+  | (n, fin.mk 1 H) := proof homomorphism.struct (πₛ→[n] (spoint f)) qed
+  | (n, fin.mk 2 H) := proof homomorphism.struct
+        (homomorphism_LES_of_homotopy_groups_fun (f (2 - n)) (1, 2) ∘g
+         homomorphism_change_fun (πg_glue Y n) _ (πg_glue_homotopy_π_glue Y n)) qed
   | (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
 
   -- In the comments below is a start on an explicit description of the LES for spectra
diff --git a/homotopy/spherical_fibrations.hlean b/homotopy/spherical_fibrations.hlean
index 2dab9b5..c6e274a 100644
--- a/homotopy/spherical_fibrations.hlean
+++ b/homotopy/spherical_fibrations.hlean
@@ -1,7 +1,7 @@
 import homotopy.join homotopy.smash
 
 open eq equiv trunc function bool join sphere sphere_index sphere.ops prod
-open pointed sigma smash
+open pointed sigma smash is_trunc
 
 namespace spherical_fibrations
 
@@ -18,7 +18,10 @@ namespace spherical_fibrations
   pt = pt :> BG n
 
   definition G_char (n : ℕ) : G n ≃ (S n..-1 ≃ S n..-1) :=
-  sorry
+  calc
+    G n ≃ Σ(p : S n..-1 = S n..-1), _ : sigma_eq_equiv
+    ... ≃ (S n..-1 = S n..-1) : sigma_equiv_of_is_contr_right
+    ... ≃ (S n..-1 ≃ S n..-1) : eq_equiv_equiv
 
   definition mirror (n : ℕ) : S n..-1 → G n :=
   begin
@@ -134,7 +137,7 @@ namespace spherical_fibrations
   - all bundles on S 3 are trivial, incl. tangent bundle
   - Adams' result on vector fields on spheres:
      there are maximally ρ(n)-1 indep.sections of the tangent bundle of S (n-1)
-     where ρ(n) is the n'th Radon-Hurwitz number.→ 
+     where ρ(n) is the n'th Radon-Hurwitz number.→
 -/
 
 -- tangent bundle on S 2:
diff --git a/homotopy/splice.hlean b/homotopy/splice.hlean
index 0066390..3524106 100644
--- a/homotopy/splice.hlean
+++ b/homotopy/splice.hlean
@@ -63,31 +63,7 @@ begin
   { exact dif_pos p}
 end
 
---   definition splice_type {N M : succ_str} (G : N → chain_complex M) (k : ℕ) (m : M)
---     (x : stratified N k) : Set* :=
---   G x.1 (iterate S (val x.2) m)
-
--- --   definition splice_map {N M : succ_str} (G : N → chain_complex M) (k : ℕ) (m : M)
--- --     (x : stratified N k) : Set* :=
--- --   G x.1 (iterate S (val x.2) m)
-
---   definition splice (N M : succ_str) (G : N → chain_complex M) (k : ℕ) (m : M)
---     (e0 : Πn, G n m ≃* G (S n) (S (iterate S k m))) :
---     chain_complex (stratified N k) :=
---   chain_complex.mk (splice_type G k m)
---     begin
---       intro x, cases x with n l, cases l with l H,
---       refine if K : l = k then _ else _,
---       { intro p, induction p, exact sorry},
---       { exact sorry}
---       -- cases l with l,
---       -- { },
---       -- { }
---     end
---     begin
---       exact sorry
---     end
-
+  --move
   definition succ_str.add [reducible] {N : succ_str} (n : N) (k : ℕ) : N :=
   iterate S k n