diff --git a/homotopy/pointed_cubes.hlean b/homotopy/pointed_cubes.hlean
index f38c547..5266db8 100644
--- a/homotopy/pointed_cubes.hlean
+++ b/homotopy/pointed_cubes.hlean
@@ -5,8 +5,8 @@ Authors: Egbert Rijke
 
 -/
 
-/- 
-The goal of this file is to extend the library of pointed types and pointed maps to support the library of prespectra 
+/-
+The goal of this file is to extend the library of pointed types and pointed maps to support the library of prespectra
 
 -/
 
@@ -37,14 +37,14 @@ end
 definition psquare_of_pid_top_bot {A B : Type*} {fleft : A →* B} {fright : A →* B} (phtpy : fright ~* fleft) : psquare (pid A) (pid B) fleft fright :=
 psquare_of_phomotopy ((pcompose_pid fright) ⬝* phtpy ⬝* (pid_pcompose fleft)⁻¹*)
 
-print psquare_of_pid_top_bot
+--print psquare_of_pid_top_bot
 
 --λ phtpy, psquare_of_phomotopy ((pid_pcompose fleft) ⬝* phtpy ⬝* ((pcompose_pid fright)⁻¹*))
 
 definition psquare_of_pid_left_right {A B : Type*} {ftop : A →* B} {fbot : A →* B} (phtpy : ftop ~* fbot) : psquare ftop fbot (pid A) (pid B) :=
 psquare_of_phomotopy ((pid_pcompose ftop) ⬝* phtpy ⬝* ((pcompose_pid fbot)⁻¹*))
 
-print psquare_of_pid_left_right
+--print psquare_of_pid_left_right
 
 definition psquare_hcompose {A B C D E F : Type*} {ftop : A →* B} {fbot : D →* E} {fleft : A →* D} {fright : B →* E} {gtop : B →* C} {gbot : E →* F} {gright : C →* F} (psq_left : psquare ftop fbot fleft fright) (psq_right : psquare gtop gbot fright gright) : psquare (gtop ∘* ftop) (gbot ∘* fbot) fleft gright :=
 begin
@@ -100,7 +100,7 @@ phsquare (pwhisker_left fright phtpy_top) (pwhisker_right fleft phtpy_bot) psq_b
 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
 
-print pinv_right_phomotopy_of_phomotopy
+--print pinv_right_phomotopy_of_phomotopy
 
 definition psquare_inv_top_bot {A B C D : Type*} {ftop : A ≃* B} {fbot : C ≃* D} {fleft : A →* C} {fright : B →* D} (psq : psquare ftop fbot fleft fright) : psquare ftop⁻¹ᵉ* fbot⁻¹ᵉ* fright fleft :=
 begin
@@ -114,25 +114,25 @@ end
 definition p2homotopy_ty_respect_pt {A B : Type*} {f g : A →* B} {H K : f ~* g} (htpy : H ~ K) : Type :=
   begin
     induction H with H p, exact p
-  end  = whisker_right (respect_pt g) (htpy pt) ⬝  
+  end  = whisker_right (respect_pt g) (htpy pt) ⬝
   begin
 induction K with K q, exact q
   end
 
-print p2homotopy_ty_respect_pt
+--print p2homotopy_ty_respect_pt
 
 structure p2homotopy {A B : Type*} {f g : A →* B} (H K : f ~* g) : Type :=
 ( to_2htpy : H ~ K)
 ( respect_pt  : p2homotopy_ty_respect_pt to_2htpy)
 
-definition ptube_v_phtpy_bot {A B C D : Type*} 
-  {ftop ftop' : A →* B} {phtpy_top : ftop ~* ftop'} 
+definition ptube_v_phtpy_bot {A B C D : Type*}
+  {ftop ftop' : A →* B} {phtpy_top : ftop ~* ftop'}
   {fbot fbot' : C →* D} {phtpy_bot phtpy_bot' : fbot ~* fbot'} (ppi_htpy_bot : phtpy_bot ~~* phtpy_bot')
-  {fleft : A →* C} {fright : B →* D} 
-  {psq_back : psquare ftop fbot fleft fright} 
-  {psq_front : psquare ftop' fbot' fleft fright} 
-  (ptb : ptube_v phtpy_top phtpy_bot psq_back psq_front)  
-  : ptube_v phtpy_top phtpy_bot' psq_back psq_front 
+  {fleft : A →* C} {fright : B →* D}
+  {psq_back : psquare ftop fbot fleft fright}
+  {psq_front : psquare ftop' fbot' fleft fright}
+  (ptb : ptube_v phtpy_top phtpy_bot psq_back psq_front)
+  : ptube_v phtpy_top phtpy_bot' psq_back psq_front
   :=
 begin
   induction ppi_htpy_bot using ppi_homotopy_rec_on_idp,
@@ -146,12 +146,12 @@ begin
   exact id,
 end
 
-definition ptube_v_left_inv {A B C D : Type*} {ftop : A ≃* B} {fbot : C ≃* D} {fleft : A →* C} {fright : B →* D} 
-  (psq : psquare ftop fbot fleft fright) : 
-  ptube_v 
-    (pleft_inv ftop) 
-    (pleft_inv fbot) 
-    (psquare_hcompose psq (psquare_inv_top_bot psq)) 
+definition ptube_v_left_inv {A B C D : Type*} {ftop : A ≃* B} {fbot : C ≃* D} {fleft : A →* C} {fright : B →* D}
+  (psq : psquare ftop fbot fleft fright) :
+  ptube_v
+    (pleft_inv ftop)
+    (pleft_inv fbot)
+    (psquare_hcompose psq (psquare_inv_top_bot psq))
     (psquare_of_pid_top_bot phomotopy.rfl) :=
 begin
   refine ptube_v_phtpy_bot _ _,
diff --git a/homotopy/strunc.hlean b/homotopy/strunc.hlean
index 6b95c84..d611093 100644
--- a/homotopy/strunc.hlean
+++ b/homotopy/strunc.hlean
@@ -210,8 +210,8 @@ end
 open option
 definition is_strunc_add_point_spectrum {X : Type} {Y : X → spectrum} {s₀ : ℤ}
   (H : Πx, is_strunc s₀ (Y x)) : Π(x : X₊), is_strunc s₀ (add_point_spectrum Y x)
-| (some x) := H x
-| none     := is_strunc_sunit s₀
+| (some x) := proof H x qed
+| none     := begin intro k, apply is_trunc_lift, apply is_trunc_unit end
 
 definition is_strunc_EM_spectrum (G : AbGroup)
   : is_strunc 0 (EM_spectrum G) :=