diff --git a/homotopy/pointed_cubes.hlean b/homotopy/pointed_cubes.hlean
index 90d49d2..02021f0 100644
--- a/homotopy/pointed_cubes.hlean
+++ b/homotopy/pointed_cubes.hlean
@@ -90,3 +90,9 @@ begin
   refine (pconst_pcompose ftop) ⬝* _,
   exact (pconst_pcompose fleft)⁻¹*,
 end
+
+definition ptube_v {A B C D : Type*} {ftop ftop' : A →* B} (phtpy_top : ftop ~* ftop') {fbot fbot' : C →* D} (phtpy_bot : fbot ~* fbot') {fleft : A →* C} {fright : B →* D} (psq_back : psquare ftop fbot fleft fright) (psq_front : psquare ftop' fbot' fleft fright) : Type :=
+phsquare (pwhisker_left fright phtpy_top) (pwhisker_right fleft phtpy_bot) psq_back psq_front
+
+definition ptube_h {A B C D : Type*} {ftop : A →* B} {fbot : C →* D} {fleft fleft' : A →* C} (phtpy_left : fleft ~* fleft') {fright fright' : B →* D} (phtpy_right : fright ~* fright') (psq_back : psquare ftop fbot fleft fright) (psq_front : psquare ftop fbot fleft' fright') : Type :=
+phsquare (pwhisker_right ftop phtpy_right) (pwhisker_left fbot phtpy_left) psq_back psq_front
diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 0e8f034..3f019a2 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -201,11 +201,18 @@ namespace spectrum
 
   structure shomotopy {N : succ_str} {E F : gen_prespectrum N} (f g : E →ₛ F) :=
     (to_phomotopy : Πn, f n ~* g n)
-    (glue_homotopy : Πn, phsquare
+    (glue_homotopy : Πn, ptube_v 
+                           (to_phomotopy n) 
+                           (ap1_phomotopy (to_phomotopy (S n))) 
+                           (glue_square f n) 
+                           (glue_square g n))
+
+/-    (glue_homotopy : Πn, phsquare
                          (pwhisker_left (glue F n) (to_phomotopy n))
                          (pwhisker_right (glue E n) (ap1_phomotopy (to_phomotopy (S n))))
                          (glue_square f n)
                          (glue_square g n))
+-/
 
   infix ` ~ₛ `:50 := shomotopy