diff --git a/homotopy/smash_assoc.hlean b/archive/smash_assoc.hlean
similarity index 99%
rename from homotopy/smash_assoc.hlean
rename to archive/smash_assoc.hlean
index 406fcaf..772bd3d 100644
--- a/homotopy/smash_assoc.hlean
+++ b/archive/smash_assoc.hlean
@@ -1,7 +1,7 @@
 -- Authors: Floris van Doorn
 -- In collaboration with Stefano, Robin
 
-import .smash
+import ..homotopy.smash
 
 open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
      function red_susp unit sigma
diff --git a/archive/smash_old.hlean b/archive/smash_old.hlean
new file mode 100644
index 0000000..fff8b18
--- /dev/null
+++ b/archive/smash_old.hlean
@@ -0,0 +1,190 @@
+ /- below are some old tries to compute (A ∧ S¹) directly -/
+
+exit
+
+  /- smash A S¹ = red_susp A -/
+
+  definition red_susp_of_smash_pcircle [unfold 2] (x : smash A S¹*) : red_susp A :=
+  begin
+    induction x using smash.elim,
+    { induction b, exact base, exact equator a },
+    { exact base },
+    { exact base },
+    { reflexivity },
+    { exact circle_elim_constant equator_pt b }
+  end
+
+  definition smash_pcircle_of_red_susp [unfold 2] (x : red_susp A) : smash A S¹* :=
+  begin
+    induction x,
+    { exact pt },
+    { exact gluel' pt a ⬝ ap (smash.mk a) loop ⬝ gluel' a pt },
+    { refine !con.right_inv ◾ _ ◾ !con.right_inv,
+      exact ap_is_constant gluer loop ⬝ !con.right_inv }
+  end
+
+  definition smash_pcircle_of_red_susp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) :
+    smash_pcircle_of_red_susp (red_susp_of_smash_pcircle (smash.mk a x)) = smash.mk a x :=
+  begin
+    induction x,
+    { exact gluel' pt a },
+    { exact abstract begin apply eq_pathover,
+      refine ap_compose smash_pcircle_of_red_susp _ _ ⬝ph _,
+      refine ap02 _ (elim_loop pt (equator a)) ⬝ !elim_equator ⬝ph _,
+      -- make everything below this a lemma defined by path induction?
+      refine !con_idp⁻¹ ⬝pv _, refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, apply whisker_lb,
+      apply whisker_tl, apply hrfl end end }
+  end
+
+  definition concat2o [unfold 10] {A B : Type} {f g h : A → B} {q : f ~ g} {r : g ~ h} {a a' : A}
+    {p : a = a'} (s : q a =[p] q a') (t : r a =[p] r a') : q a ⬝ r a =[p] q a' ⬝ r a' :=
+  by induction p; exact idpo
+
+  definition apd_con_fn [unfold 10] {A B : Type} {f g h : A → B} {q : f ~ g} {r : g ~ h} {a a' : A}
+    (p : a = a') : apd (λa, q a ⬝ r a) p = concat2o (apd q p) (apd r p) :=
+  by induction p; reflexivity
+
+  -- definition apd_con_fn_constant [unfold 10] {A B : Type} {f : A → B} {b b' : B} {q : Πa, f a = b}
+  --   {r : b = b'} {a a' : A} (p : a = a') :
+  --   apd (λa, q a ⬝ r) p = concat2o (apd q p) (pathover_of_eq _ idp) :=
+  -- by induction p; reflexivity
+
+
+  definition smash_pcircle_pequiv_red [constructor] (A : Type*) : smash A S¹* ≃* red_susp A :=
+  begin
+    fapply pequiv_of_equiv,
+    { fapply equiv.MK,
+      { exact red_susp_of_smash_pcircle },
+      { exact smash_pcircle_of_red_susp },
+      { exact abstract begin intro x, induction x,
+        { reflexivity },
+        { apply eq_pathover, apply hdeg_square,
+          refine ap_compose red_susp_of_smash_pcircle _ _ ⬝ ap02 _ !elim_equator ⬝ _ ⬝ !ap_id⁻¹,
+          refine !ap_con ⬝ (!ap_con ⬝ !elim_gluel' ◾ !ap_compose'⁻¹) ◾ !elim_gluel' ⬝ _,
+          esimp, exact !idp_con ⬝ !elim_loop },
+        { exact sorry } end end },
+      { intro x, induction x,
+        { exact smash_pcircle_of_red_susp_of_smash_pcircle_pt a b },
+        { exact gluel pt },
+        { exact gluer pt },
+        { apply eq_pathover_id_right,
+          refine ap_compose smash_pcircle_of_red_susp _ _ ⬝ph _,
+          unfold [red_susp_of_smash_pcircle],
+          refine ap02 _ !elim_gluel ⬝ph _,
+          esimp, apply whisker_rt, exact vrfl },
+        { apply eq_pathover_id_right,
+          refine ap_compose smash_pcircle_of_red_susp _ _ ⬝ph _,
+          unfold [red_susp_of_smash_pcircle],
+          -- not sure why so many implicit arguments are needed here...
+          refine ap02 _ (@smash.elim_gluer A S¹* _ (λa, circle.elim red_susp.base (equator a)) red_susp.base red_susp.base (λa, refl red_susp.base) (circle_elim_constant equator_pt) b) ⬝ph _,
+          apply square_of_eq, induction b,
+          { exact whisker_right _ !con.right_inv },
+          { apply eq_pathover_dep, refine !apd_con_fn ⬝pho _ ⬝hop !apd_con_fn⁻¹,
+            refine ap (λx, concat2o x _) !rec_loop ⬝pho _ ⬝hop (ap011 concat2o (apd_compose1 (λa b, ap smash_pcircle_of_red_susp b) (circle_elim_constant equator_pt) loop) !apd_constant')⁻¹,
+            exact sorry }
+
+          }}},
+    { reflexivity }
+  end
+
+  /- smash A S¹ = susp A -/
+  open susp
+
+
+  definition psusp_of_smash_pcircle [unfold 2] (x : smash A S¹*) : psusp A :=
+  begin
+    induction x using smash.elim,
+    { induction b, exact pt, exact merid a ⬝ (merid pt)⁻¹ },
+    { exact pt },
+    { exact pt },
+    { reflexivity },
+    { induction b, reflexivity, apply eq_pathover_constant_right, apply hdeg_square,
+      exact !elim_loop ⬝ !con.right_inv }
+  end
+
+  definition smash_pcircle_of_psusp [unfold 2] (x : psusp A) : smash A S¹* :=
+  begin
+    induction x,
+    { exact pt },
+    { exact pt },
+    { exact gluel' pt a ⬝ (ap (smash.mk a) loop ⬝ gluel' a pt) },
+  end
+
+ -- the definitions below compile, but take a long time to do so and have sorry's in them
+  definition smash_pcircle_of_psusp_of_smash_pcircle_pt [unfold 3] (a : A) (x : S¹*) :
+    smash_pcircle_of_psusp (psusp_of_smash_pcircle (smash.mk a x)) = smash.mk a x :=
+  begin
+    induction x,
+    { exact gluel' pt a },
+    { exact abstract begin apply eq_pathover,
+      refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _,
+      refine ap02 _ (elim_loop north (merid a ⬝ (merid pt)⁻¹)) ⬝ph _,
+      refine !ap_con ⬝ (!elim_merid ◾ (!ap_inv ⬝ !elim_merid⁻²)) ⬝ph _,
+      -- make everything below this a lemma defined by path induction?
+      exact sorry,
+      -- refine !con_idp⁻¹ ⬝pv _, apply whisker_tl, refine !con.assoc⁻¹ ⬝ph _,
+      -- apply whisker_bl, apply whisker_lb,
+      -- refine !con_idp⁻¹ ⬝pv _, apply whisker_tl, apply hrfl
+      -- refine !con_idp⁻¹ ⬝pv _, apply whisker_tl,
+      -- refine !con.assoc⁻¹ ⬝ph _, apply whisker_bl, apply whisker_lb, apply hrfl
+      -- apply square_of_eq, rewrite [+con.assoc], apply whisker_left, apply whisker_left,
+      -- symmetry, apply con_eq_of_eq_inv_con, esimp, apply con_eq_of_eq_con_inv,
+      -- refine _⁻² ⬝ !con_inv, refine _ ⬝ !con.assoc,
+      -- refine _ ⬝ whisker_right _ !inv_con_cancel_right⁻¹, refine _ ⬝ !con.right_inv⁻¹,
+      -- refine !con.right_inv ◾ _, refine _ ◾ !con.right_inv,
+      -- refine !ap_mk_right ⬝ !con.right_inv
+      end end }
+  end
+
+  -- definition smash_pcircle_of_psusp_of_smash_pcircle_gluer_base (b : S¹*)
+  --   : square (smash_pcircle_of_psusp_of_smash_pcircle_pt (Point A) b)
+  --            (gluer pt)
+  --            (ap smash_pcircle_of_psusp (ap (λ a, psusp_of_smash_pcircle a) (gluer b)))
+  --            (gluer b) :=
+  -- begin
+  --   refine ap02 _ !elim_gluer ⬝ph _,
+  --   induction b,
+  --   { apply square_of_eq, exact whisker_right _ !con.right_inv },
+  --   { apply square_pathover', exact sorry }
+  -- end
+
+exit
+  definition smash_pcircle_pequiv [constructor] (A : Type*) : smash A S¹* ≃* psusp A :=
+  begin
+    fapply pequiv_of_equiv,
+    { fapply equiv.MK,
+      { exact psusp_of_smash_pcircle },
+      { exact smash_pcircle_of_psusp },
+      { exact abstract begin intro x, induction x,
+        { reflexivity },
+        { exact merid pt },
+        { apply eq_pathover_id_right,
+          refine ap_compose psusp_of_smash_pcircle _ _ ⬝ph _,
+          refine ap02 _ !elim_merid ⬝ph _,
+          rewrite [↑gluel', +ap_con, +ap_inv, -ap_compose'],
+          refine (_ ◾ _⁻² ◾ _ ◾ (_ ◾ _⁻²)) ⬝ph _,
+          rotate 5, do 2 (unfold [psusp_of_smash_pcircle]; apply elim_gluel),
+          esimp, apply elim_loop, do 2 (unfold [psusp_of_smash_pcircle]; apply elim_gluel),
+          refine idp_con (merid a ⬝ (merid (Point A))⁻¹) ⬝ph _,
+          apply square_of_eq, refine !idp_con ⬝ _⁻¹, apply inv_con_cancel_right } end end },
+      { intro x, induction x using smash.rec,
+        { exact smash_pcircle_of_psusp_of_smash_pcircle_pt a b },
+        { exact gluel pt },
+        { exact gluer pt },
+        { apply eq_pathover_id_right,
+          refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _,
+          unfold [psusp_of_smash_pcircle],
+          refine ap02 _ !elim_gluel ⬝ph _,
+          esimp, apply whisker_rt, exact vrfl },
+        { apply eq_pathover_id_right,
+          refine ap_compose smash_pcircle_of_psusp _ _ ⬝ph _,
+          unfold [psusp_of_smash_pcircle],
+          refine ap02 _ !elim_gluer ⬝ph _,
+          induction b,
+          { apply square_of_eq, exact whisker_right _ !con.right_inv },
+          { exact sorry}
+          }}},
+    { reflexivity }
+  end
+
+end smash
diff --git a/homotopy/sample.hlean b/homotopy/sample.hlean
deleted file mode 100644
index 54a787c..0000000
--- a/homotopy/sample.hlean
+++ /dev/null
@@ -1,194 +0,0 @@
-/-
-Copyright (c) 2015 Ulrik Buchholtz. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Ulrik Buchholtz
--/
-import types.trunc types.arrow_2 types.fiber homotopy.susp
-
-open eq is_trunc is_equiv nat equiv trunc function fiber
-
-namespace homotopy
-
-  definition is_conn [reducible] (n : trunc_index) (A : Type) : Type :=
-  is_contr (trunc n A)
-
-  definition is_conn_equiv_closed (n : trunc_index) {A B : Type}
-    : A ≃ B → is_conn n A → is_conn n B :=
-  begin
-    intros H C,
-    fapply @is_contr_equiv_closed (trunc n A) _,
-    apply trunc_equiv_trunc,
-    assumption
-  end
-
-  definition is_conn_fun (n : trunc_index) {A B : Type} (f : A → B) : Type :=
-  Πb : B, is_conn n (fiber f b)
-
-  namespace is_conn_fun
-  section
-    parameters {n : trunc_index} {A B : Type} {h : A → B}
-               (H : is_conn_fun n h) (P : B → n -Type)
-
-    private definition helper : (Πa : A, P (h a)) → Πb : B, trunc n (fiber h b) → P b :=
-    λt b, trunc.rec (λx, point_eq x ▸ t (point x))
-
-    private definition g : (Πa : A, P (h a)) → (Πb : B, P b) :=
-    λt b, helper t b (@center (trunc n (fiber h b)) (H b))
-
-    -- induction principle for n-connected maps (Lemma 7.5.7)
-    definition rec : is_equiv (λs : Πb : B, P b, λa : A, s (h a)) :=
-    adjointify (λs a, s (h a)) g
-    begin
-      intro t, apply eq_of_homotopy, intro a, unfold g, unfold helper,
-      rewrite [@center_eq _ (H (h a)) (tr (fiber.mk a idp))],
-    end
-    begin
-      intro k, apply eq_of_homotopy, intro b, unfold g,
-      generalize (@center _ (H b)), apply trunc.rec, apply fiber.rec,
-      intros a p, induction p, reflexivity
-    end
-
-    definition elim : (Πa : A, P (h a)) → (Πb : B, P b) :=
-    @is_equiv.inv _ _ (λs a, s (h a)) rec
-
-    definition elim_β : Πf : (Πa : A, P (h a)), Πa : A, elim f (h a) = f a :=
-    λf, apd10 (@is_equiv.right_inv _ _ (λs a, s (h a)) rec f)
-
-  end
-
-  section
-    universe variables u v
-    parameters {n : trunc_index} {A : Type.{u}} {B : Type.{v}} {h : A → B}
-    parameter sec : ΠP : B → trunctype.{max u v} n,
-                    is_retraction (λs : (Πb : B, P b), λ a, s (h a))
-
-    private definition s := sec (λb, trunctype.mk' n (trunc n (fiber h b)))
-
-    include sec
-
-    -- the other half of Lemma 7.5.7
-    definition intro : is_conn_fun n h :=
-    begin
-      intro b,
-      apply is_contr.mk (@is_retraction.sect _ _ _ s (λa, tr (fiber.mk a idp)) b),
-      esimp, apply trunc.rec, apply fiber.rec, intros a p,
-      apply transport
-               (λz : (Σy, h a = y), @sect _ _ _ s (λa, tr (mk a idp)) (sigma.pr1 z) =
-                                    tr (fiber.mk a (sigma.pr2 z)))
-               (@center_eq _ (is_contr_sigma_eq (h a)) (sigma.mk b p)),
-      exact apd10 (@right_inverse _ _ _ s (λa, tr (fiber.mk a idp))) a
-    end
-  end
-  end is_conn_fun
-
-  -- Connectedness is related to maps to and from the unit type, first to
-  section
-    parameters (n : trunc_index) (A : Type)
-
-    definition is_conn_of_map_to_unit
-      : is_conn_fun n (λx : A, unit.star) → is_conn n A :=
-    begin
-      intro H, unfold is_conn_fun at H,
-      rewrite [-(ua (fiber.fiber_star_equiv A))],
-      exact (H unit.star)
-    end
-
-    -- now maps from unit
-    definition is_conn_of_map_from_unit (a₀ : A) (H : is_conn_fun n (const unit a₀))
-      : is_conn n .+1 A :=
-    is_contr.mk (tr a₀)
-    begin
-      apply trunc.rec, intro a,
-      exact trunc.elim (λz : fiber (const unit a₀) a, ap tr (point_eq z))
-                            (@center _ (H a))
-    end
-
-    definition is_conn_fun_from_unit (a₀ : A) [H : is_conn n .+1 A]
-      : is_conn_fun n (const unit a₀) :=
-    begin
-      intro a,
-      apply is_conn_equiv_closed n (equiv.symm (fiber_const_equiv A a₀ a)),
-      apply @is_contr_equiv_closed _ _ (tr_eq_tr_equiv n a₀ a),
-    end
-
-  end
-
-  -- Lemma 7.5.2
-  definition minus_one_conn_of_surjective {A B : Type} (f : A → B)
-    : is_surjective f → is_conn_fun -1 f :=
-  begin
-    intro H, intro b,
-    exact @is_contr_of_inhabited_prop (∥fiber f b∥) (is_trunc_trunc -1 (fiber f b)) (H b),
-  end
-
-  definition is_surjection_of_minus_one_conn {A B : Type} (f : A → B)
-    : is_conn_fun -1 f → is_surjective f :=
-  begin
-    intro H, intro b,
-    exact @center (∥fiber f b∥) (H b),
-  end
-
-  definition merely_of_minus_one_conn {A : Type} : is_conn -1 A → ∥A∥ :=
-  λH, @center (∥A∥) H
-
-  definition minus_one_conn_of_merely {A : Type} : ∥A∥ → is_conn -1 A :=
-  @is_contr_of_inhabited_prop (∥A∥) (is_trunc_trunc -1 A)
-
-  section
-    open arrow
-
-    variables {f g : arrow}
-
-    -- Lemma 7.5.4
-    definition retract_of_conn_is_conn [instance] (r : arrow_hom f g) [H : is_retraction r]
-      (n : trunc_index) [K : is_conn_fun n f] : is_conn_fun n g :=
-    begin
-      intro b, unfold is_conn,
-      apply is_contr_retract (trunc_functor n (retraction_on_fiber r b)),
-      exact K (on_cod (arrow.is_retraction.sect r) b)
-    end
-
-  end
-
-  -- Corollary 7.5.5
-  definition is_conn_homotopy (n : trunc_index) {A B : Type} {f g : A → B}
-    (p : f ~ g) (H : is_conn_fun n f) : is_conn_fun n g :=
-  @retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H
-
-  -- all types are -2-connected
-  definition minus_two_conn [instance] (A : Type) : is_conn -2 A :=
-  _
-
-  -- Theorem 8.2.1
-  open susp
-
-  definition is_conn_susp [instance] (n : trunc_index) (A : Type)
-    [H : is_conn n A] : is_conn (n .+1) (susp A) :=
-  is_contr.mk (tr north)
-  begin
-    apply trunc.rec,
-    fapply susp.rec,
-    { reflexivity },
-    { exact (trunc.rec (λa, ap tr (merid a)) (center (trunc n A))) },
-    { intro a,
-      generalize (center (trunc n A)),
-      apply trunc.rec,
-      intro a',
-      apply pathover_of_tr_eq,
-      rewrite [eq_transport_Fr,idp_con],
-      revert H, induction n with [n, IH],
-      { intro H, apply is_prop.elim },
-      { intros H,
-        change ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid a'),
-        generalize a',
-        apply is_conn_fun.elim
-              (is_conn_fun_from_unit n A a)
-              (λx : A, trunctype.mk' n (ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid x))),
-        intros,
-        change ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid a),
-        reflexivity
-      }
-    }
-  end
-
-end homotopy
diff --git a/homotopy/smash_adjoint.hlean b/homotopy/smash_adjoint.hlean
index 6213abb..112e54d 100644
--- a/homotopy/smash_adjoint.hlean
+++ b/homotopy/smash_adjoint.hlean
@@ -548,5 +548,4 @@ namespace smash
     rexact phomotopy_of_eq ((smash_assoc_elim_equiv_natural_left _ f g h)⁻¹ʰ* !pid)⁻¹
   end
 
-
 end smash
diff --git a/homotopy/temp2.hlean b/homotopy/temp2.hlean
deleted file mode 100644
index 5569161..0000000
--- a/homotopy/temp2.hlean
+++ /dev/null
@@ -1,123 +0,0 @@
-
-import .smash_adjoint
-
-open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber prod.ops wedge is_trunc
-     function red_susp unit smash
-
-variables {A A' B B' C C' D E F X X' : Type*}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- definition concat2o {A B : Type} {f g h : A → B} {a₁ a₂ : A} {p₁ : f a₁ = g a₁} {p₂ : f a₂ = g a₂}
---   {q₁ : g a₁ = h a₁} {q₂ : g a₂ = h a₂} {r : a₁ = a₂} (s₁ : p₁ =[r] p₂) (s₂ : q₁ =[r] q₂) :
---   p₁ ⬝ q₁ =[r] p₂ ⬝ q₂ :=
--- apo011 (λx, concat) s₁ s₂
-
--- infixl ` ◾o' `:75 := concat2o
-
--- definition apd_con_fn {A B : Type} {f g h : A → B} {a₁ a₂ : A} (p : f ~ g) (q : g ~ h) (r : a₁ = a₂)
---   : apd (λa, p a ⬝ q a) r = apd p r ◾o' apd q r :=
--- begin
---   induction r, reflexivity
--- end
-
--- definition ap02o {A : Type} {B C : A → Type} {g h : Πa, B a} (f : Πa, B a → C a) {a₁ a₂ : A} {p₁ : g a₁ = h a₁}
---   {p₂ : g a₂ = h a₂} {q : a₁ = a₂} (r : p₁ =[q] p₂) : ap (f a₁) p₁ =[q] ap (f a₂) p₂ :=
--- apo (λx, ap (f x)) r
-
--- definition apo_eq_pathover {A A' B B' : Type} {a a' : A} {f g : A → B} {i : A → A'} {f' g' : A' → B'}
---   {p : a = a'} {q : f a = g a} (h : Πa, f a = g a → f' (i a) = g' (i a))
---   {r : f a' = g a'} (s : square q r (ap f p) (ap g p)) :
---    apo h (eq_pathover s) = eq_pathover _ :=
--- sorry
-
--- definition ap02o_eq_pathover {A A' B B' : Type} {a a' : A} {f g : A → B} {i : A → A'} {f' g' : A' → B'}
---   {p : a = a'} {q : f a = g a} (h : Πa, f a = g a → f' (i a) = g' (i a))
---   {r : f a' = g a'} (s : square q r (ap f p) (ap g p)) :
---    apo h (eq_pathover s) = eq_pathover _ :=
--- sorry
-
--- definition apd_ap_fn {A : Type} {B C : A → Type} {g h : Πa, B a} (f : Πa, B a → C a) (p : g ~ h)
---   {a₁ a₂ : A} (r : a₁ = a₂) : apd (λa, ap (f a) (p a)) r = ap02o f (apd p r) :=
--- begin
---   induction r; reflexivity
--- end
-
--- definition apd_ap_fn {A : Type} {B C : A → Type} {g h : Πa, B a} (f : Πa, B a → C a) (p : g ~ h)
---   {a₁ a₂ : A} (r : a₁ = a₂) : apd (λa, ap (f a) (p a)) r = ap02o f (apd p r) :=
diff --git a/homotopy/torus.hlean b/homotopy/torus.hlean
deleted file mode 100644
index f7314f1..0000000
--- a/homotopy/torus.hlean
+++ /dev/null
@@ -1,80 +0,0 @@
-import homotopy.torus
-
-open eq circle prod prod.ops function
-
-namespace torus
-
-  definition S1xS1_of_torus [unfold 1] (x : T²) : S¹ × S¹ :=
-  begin
-    induction x,
-    { exact (circle.base, circle.base) },
-    { exact prod_eq loop idp },
-    { exact prod_eq idp loop },
-    { apply square_of_eq,
-      exact !prod_eq_concat ⬝ ap011 prod_eq !idp_con⁻¹ !idp_con ⬝ !prod_eq_concat⁻¹ }
-  end
-
-  definition torus_of_S1xS1 [unfold 1] (x : S¹ × S¹) : T² :=
-  begin
-    induction x with x y, induction x,
-    { induction y,
-      { exact base },
-      { exact loop2 }},
-    { induction y,
-      { exact loop1 },
-      { apply eq_pathover, refine !elim_loop ⬝ph surf ⬝hp !elim_loop⁻¹ }}
-  end
-
-  definition to_from_base_left [unfold 1] (y : S¹) :
-    S1xS1_of_torus (torus_of_S1xS1 (circle.base, y)) = (circle.base, y) :=
-  begin
-    induction y,
-    { reflexivity },
-    { apply eq_pathover, apply hdeg_square,
-      refine ap_compose S1xS1_of_torus _ _ ⬝ ap02 _ !elim_loop ⬝ _ ⬝ !ap_prod_mk_right⁻¹,
-      apply elim_loop2 }
-  end
-
-  definition from_to_loop1
-    : pathover (λa, torus_of_S1xS1 (S1xS1_of_torus a) = a) proof idp qed loop1 proof idp qed :=
-  begin
-    apply eq_pathover, apply hdeg_square,
-    refine ap_compose torus_of_S1xS1 _ _ ⬝ ap02 _ !elim_loop1 ⬝ _ ⬝ !ap_id⁻¹,
-    refine !ap_prod_elim ⬝ !idp_con ⬝ !elim_loop
-  end
-
-  definition from_to_loop2
-    : pathover (λa, torus_of_S1xS1 (S1xS1_of_torus a) = a) proof idp qed loop2 proof idp qed :=
-  begin
-    apply eq_pathover, apply hdeg_square,
-    refine ap_compose torus_of_S1xS1 _ _ ⬝ ap02 _ !elim_loop2 ⬝ _ ⬝ !ap_id⁻¹,
-    refine !ap_prod_elim ⬝ !elim_loop
-  end
-
-  definition torus_equiv_S1xS1 : T² ≃ S¹ × S¹ :=
-  begin
-    fapply equiv.MK,
-    { exact S1xS1_of_torus },
-    { exact torus_of_S1xS1 },
-    { intro x, induction x with x y, induction x,
-      { exact to_from_base_left y },
-      { apply eq_pathover,
-        refine ap_compose (S1xS1_of_torus ∘ torus_of_S1xS1) _ _ ⬝ph _,
-        refine ap02 _ !ap_prod_mk_left ⬝ph _ ⬝hp !ap_prod_mk_left⁻¹,
-        refine !ap_compose ⬝ ap02 _ (!ap_prod_elim ⬝ !idp_con) ⬝ph _,
-        refine ap02 _ !elim_loop ⬝ph _,
-        induction y,
-        { apply hdeg_square, apply elim_loop1 },
-        { apply square_pathover, exact sorry }
-        -- apply square_of_eq, induction y,
-        -- { refine !idp_con ⬝ !elim_loop1⁻¹ },
-        -- { apply eq_pathover_dep, }
-        }},
-    { intro x, induction x,
-      { reflexivity },
-      { exact from_to_loop1 },
-      { exact from_to_loop2 },
-      { exact sorry }}
-  end
-
-end torus
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index b50f404..b133f06 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -5,14 +5,6 @@ import homotopy.sphere2 homotopy.cofiber homotopy.wedge
 open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
      is_trunc function sphere unit sum prod
 
-attribute equiv_unit_of_is_contr [constructor]
-attribute pwedge pushout.symm pushout.equiv pushout.is_equiv_functor [constructor]
-attribute is_succ_add_right is_succ_add_left is_succ_bit0 [constructor]
-attribute pushout.functor [unfold 16]
-attribute pushout.transpose [unfold 6]
-attribute ap_eq_apd10 [unfold 5]
-attribute eq_equiv_eq_symm [constructor]
-
 definition add_comm_right {A : Type} [add_comm_semigroup A] (n m k : A) : n + m + k = n + k + m :=
 !add.assoc ⬝ ap (add n) !add.comm ⬝ !add.assoc⁻¹
 
@@ -96,7 +88,6 @@ section -- squares
 
 end
 
-infix ` ⬝p2 `:75 := eq_concat2
 section -- cubes
 
   variables {A B : Type} {a₀₀₀ a₂₀₀ a₀₂₀ a₂₂₀ a₀₀₂ a₂₀₂ a₀₂₂ a₂₂₂ a a' : A}
@@ -216,7 +207,7 @@ end
   definition id_compose {A B : Type} (f : A → B) : id ∘ f ~ f :=
   by reflexivity
 
-  -- move
+  -- move to eq2
   definition ap_eq_ap011 {A B C X : Type} (f : A → B → C) (g : X → A) (h : X → B) {x x' : X}
     (p : x = x') : ap (λx, f (g x) (h x)) p = ap011 f (ap g p) (ap h p) :=
   by induction p; reflexivity