diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean
index e34213b16..98018619e 100644
--- a/hott/hit/pushout.hlean
+++ b/hott/hit/pushout.hlean
@@ -78,7 +78,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
   elim_type Pinl Pinr Pglue y
 
   theorem elim_type_glue (Pinl : BL → Type) (Pinr : TR → Type)
-    (Pglue : Π(x : TL), Pinl (f x) ≃ Pinr (g x)) (y : pushout) (x : TL)
+    (Pglue : Π(x : TL), Pinl (f x) ≃ Pinr (g x)) (x : TL)
     : transport (elim_type Pinl Pinr Pglue) (glue x) = Pglue x :=
   by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_glue];apply cast_ua_fn
 
diff --git a/hott/hit/suspension.hlean b/hott/hit/suspension.hlean
index 0fdd39096..6564a0bb8 100644
--- a/hott/hit/suspension.hlean
+++ b/hott/hit/suspension.hlean
@@ -27,7 +27,7 @@ namespace suspension
   protected definition rec {P : suspension A → Type} (PN : P !north) (PS : P !south)
     (Pm : Π(a : A), PN =[merid a] PS) (x : suspension A) : P x :=
   begin
-    fapply (pushout.rec_on _ _ x),
+    fapply pushout.rec_on _ _ x,
     { intro u, cases u, exact PN},
     { intro u, cases u, exact PS},
     { exact Pm},
@@ -66,7 +66,7 @@ namespace suspension
   suspension.elim_type PN PS Pm x
 
   theorem elim_type_merid (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
-    (x : suspension A) (a : A) : transport (suspension.elim_type PN PS Pm) (merid a) = Pm a :=
+    (a : A) : transport (suspension.elim_type PN PS Pm) (merid a) = Pm a :=
   by rewrite [tr_eq_cast_ap_fn,↑suspension.elim_type,elim_merid];apply cast_ua_fn
 
 end suspension
diff --git a/hott/hit/type_quotient.hlean b/hott/hit/type_quotient.hlean
index 776786dd6..5c9b61465 100644
--- a/hott/hit/type_quotient.hlean
+++ b/hott/hit/type_quotient.hlean
@@ -6,7 +6,12 @@ Authors: Floris van Doorn
 Type quotients (quotient without truncation)
 -/
 
-/- The hit type_quotient is primitive, declared in init.hit. -/
+/-
+  The hit type_quotient is primitive, declared in init.hit.
+  The constructors are
+    class_of : A → A / R (A implicit, R explicit)
+    eq_of_rel : R a a' → a = a' (R explicit)
+-/
 
 open eq equiv sigma.ops
 
diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean
index 9b4a2699a..b28a3b6aa 100644
--- a/hott/types/prod.hlean
+++ b/hott/types/prod.hlean
@@ -7,28 +7,21 @@ Ported from Coq HoTT
 Theorems about products
 -/
 
-open eq equiv is_equiv is_trunc prod prod.ops
+open eq equiv is_equiv is_trunc prod prod.ops unit
 
 variables {A A' B B' C D : Type}
           {a a' a'' : A} {b b₁ b₂ b' b'' : B} {u v w : A × B}
 
 namespace prod
 
-  -- prod.eta is already used for the eta rule for strict equality
-  protected definition eta (u : A × B) : (pr₁ u , pr₂ u) = u :=
+  protected definition eta (u : A × B) : (pr₁ u, pr₂ u) = u :=
   by cases u; apply idp
 
-  definition pair_eq (pa : a = a') (pb : b = b') : (a , b) = (a' , b') :=
+  definition pair_eq (pa : a = a') (pb : b = b') : (a, b) = (a', b') :=
   by cases pa; cases pb; apply idp
 
   definition prod_eq (H₁ : pr₁ u = pr₁ v) (H₂ : pr₂ u = pr₂ v) : u = v :=
-  begin
-    cases u with a₁ b₁,
-    cases v with a₂ b₂,
-    apply transport _ (prod.eta (a₁, b₁)),
-    apply transport _ (prod.eta (a₂, b₂)),
-    apply pair_eq H₁ H₂,
-  end
+  by cases u; cases v; exact pair_eq H₁ H₂
 
   /- Symmetry -/
 
@@ -41,6 +34,15 @@ namespace prod
   definition prod_comm_equiv (A B : Type) : A × B ≃ B × A :=
   equiv.mk flip _
 
+  definition prod_contr_equiv (A B : Type) [H : is_contr B] : A × B ≃ A :=
+  equiv.MK pr1
+           (λx, (x, !center))
+           (λx, idp)
+           (λx, by cases x with a b; exact pair_eq idp !center_eq)
+
+  definition prod_unit_equiv (A : Type) : A × unit ≃ A :=
+  !prod_contr_equiv
+
   -- is_trunc_prod is defined in sigma
 
 end prod
diff --git a/hott/types/square.hlean b/hott/types/square.hlean
index 5a5992d48..dbab850e4 100644
--- a/hott/types/square.hlean
+++ b/hott/types/square.hlean
@@ -64,6 +64,18 @@ namespace cubical
   definition square_of_eq (r : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂) : square p₁₀ p₁₂ p₀₁ p₂₁ :=
   by cases p₁₂; (esimp [concat] at r); cases r; cases p₂₁; cases p₁₀; exact ids
 
+  definition aps {B : Type} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
+    : square (ap f p₁₀) (ap f p₁₂) (ap f p₀₁) (ap f p₂₁) :=
+  by cases s₁₁;exact ids
+
+  definition square_of_homotopy {B : Type} {f g : A → B} (H : f ∼ g) (p : a = a')
+    : square (H a) (H a') (ap f p) (ap g p) :=
+  by cases p; apply vrefl
+
+  definition square_of_homotopy' {B : Type} {f g : A → B} (H : f ∼ g) (p : a = a')
+    : square (ap f p) (ap g p) (H a) (H a') :=
+  by cases p; apply hrefl
+
   definition square_equiv_eq (t : a₀₀ = a₀₂) (b : a₂₀ = a₂₂) (l : a₀₀ = a₂₀) (r : a₀₂ = a₂₂)
     : square t b l r ≃ t ⬝ r = l ⬝ b :=
   begin