diff --git a/homotopy/spectrum.hlean b/homotopy/spectrum.hlean
index 1ab75c4..0be9bea 100644
--- a/homotopy/spectrum.hlean
+++ b/homotopy/spectrum.hlean
@@ -194,6 +194,26 @@ namespace spectrum
 
   infix ` ~ₛ `:50 := shomotopy
 
+  definition shomotopy_compose {N : succ_str} {E F : gen_prespectrum N} {f g h : E →ₛ F} (p : g ~ₛ h) (q : f ~ₛ g) : f ~ₛ h :=
+  shomotopy.mk
+    (λn, (shomotopy.to_phomotopy q n) ⬝* (shomotopy.to_phomotopy p n))
+    begin
+      intro n,
+      rewrite (pwhisker_left_trans _),
+      rewrite ap1_phomotopy_trans,
+      rewrite (pwhisker_right_trans _),
+      exact phhconcat ((shomotopy.glue_homotopy q) n) ((shomotopy.glue_homotopy p) n)
+    end
+
+  definition shomotopy_inverse {N : succ_str} {E F : gen_prespectrum N} {f g : E →ₛ F} (p : f ~ₛ g) : g ~ₛ f :=
+  shomotopy.mk (λn, (shomotopy.to_phomotopy p n)⁻¹*) begin
+    intro n,
+    rewrite (pwhisker_left_symm _ _),
+    rewrite [-ap1_phomotopy_symm],
+    rewrite (pwhisker_right_symm _ _),
+    exact phhinverse ((shomotopy.glue_homotopy p) n)
+  end
+
   ------------------------------
   -- Suspension prespectra
   ------------------------------
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 61f54a9..7004cfb 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -562,6 +562,28 @@ end injective_surjective
 -- Yuri Sulyma's code from HoTT MRC
 
 notation `⅀→`:(max+5) := psusp_functor
+notation `⅀⇒`:(max+5) := psusp_functor_phomotopy
+notation `Ω⇒`:(max+5) := ap1_phomotopy
+
+definition ap1_phomotopy_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : (Ω⇒ p)⁻¹* = Ω⇒ (p⁻¹*) :=
+begin
+  induction p using phomotopy_rec_on_idp,
+  rewrite ap1_phomotopy_refl,
+  rewrite [+refl_symm],
+  rewrite ap1_phomotopy_refl
+end
+
+definition ap1_phomotopy_trans {A B : Type*} {f g h : A →* B} (q : g ~* h) (p : f ~* g) : Ω⇒ (p ⬝* q) = Ω⇒ p ⬝* Ω⇒ q :=
+begin
+  induction p using phomotopy_rec_on_idp,
+  induction q using phomotopy_rec_on_idp,
+  rewrite trans_refl,
+  rewrite [+ap1_phomotopy_refl],
+  rewrite trans_refl
+end
+
+definition psusp_pelim2 {X Y : Type*} {f g : ⅀ X →* Y} (p : f ~* g) : ((loop_psusp_pintro X Y) f) ~* ((loop_psusp_pintro X Y) g) :=
+pwhisker_right (loop_psusp_unit X) (Ω⇒ p)
 
 namespace pointed
   variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type*}