diff --git a/hott/homotopy/cofiber.hlean b/hott/homotopy/cofiber.hlean
index 14961d17d..d72087437 100644
--- a/hott/homotopy/cofiber.hlean
+++ b/hott/homotopy/cofiber.hlean
@@ -26,8 +26,8 @@ namespace cofiber
     { cases u, reflexivity },
     { exact !glue ⬝ ap inr (right_inv f b) },
     { apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, refine !ap_constant ⬝ph _, 
-      esimp, krewrite adj, apply move_bot_of_left, krewrite idp_con, 
-      apply transpose, refine _ ⬝hp !ap_compose, apply square_Flr_idp_ap },
+      apply move_bot_of_left, refine !idp_con ⬝ph _, apply transpose, esimp,
+      refine _ ⬝hp (ap (ap inr) !adj⁻¹), refine _ ⬝hp !ap_compose, apply square_Flr_idp_ap },
   end
 
   end
diff --git a/hott/homotopy/smash.hlean b/hott/homotopy/smash.hlean
new file mode 100644
index 000000000..172a94ae6
--- /dev/null
+++ b/hott/homotopy/smash.hlean
@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2016 Jakob von Raumer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jakob von Raumer
+
+The Smash Product of Types
+-/
+
+import hit.pushout .wedge .cofiber .susp .sphere
+
+open eq pushout prod pointed Pointed
+
+definition product_of_wedge (A B : Type*) : Wedge A B →* A ×* B :=
+begin
+  fconstructor,
+  intro x, induction x with [a, b], exact (a, point B), exact (point A, b), 
+  do 2 reflexivity
+end
+
+definition Smash (A B : Type*) := Cofiber (product_of_wedge A B)
+
+open sphere susp
+
+namespace smash
+
+  definition susp_equiv_circle_smash (X : Type*) : Susp X ≃* Smash (Sphere 1) X :=
+  sorry  
+
+end smash
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index 6438ce695..94c8bc745 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -57,6 +57,11 @@ namespace pointed
   definition pointed_bool [instance] [constructor] : pointed bool :=
   pointed.mk ff
 
+  definition Prod [constructor] (A B : Type*) : Type* :=
+  pointed.mk' (A × B)
+
+  infixr ` ×* `:35 := Prod
+
   definition Bool [constructor] : Type* :=
   pointed.mk' bool