diff --git a/hott/algebra/category/constructions/set.hlean b/hott/algebra/category/constructions/set.hlean
index 826bee75f..fc51ac1bc 100644
--- a/hott/algebra/category/constructions/set.hlean
+++ b/hott/algebra/category/constructions/set.hlean
@@ -44,7 +44,7 @@ namespace category
       : is_equiv (@iso_of_equiv A B) :=
     adjointify _ (λf, equiv_of_iso f)
                  (λf, proof iso_eq idp qed)
-                 (λf, equiv_eq idp)
+                 (λf, equiv_eq' idp)
 
     local attribute is_equiv_iso_of_equiv [instance]
 
@@ -60,7 +60,7 @@ namespace category
                            (ap10 (to_right_inverse f))
                            (ap10 (to_left_inverse  f)) qed)
              (λf, proof iso_eq idp qed)
-             (λf, proof equiv_eq idp qed)
+             (λf, proof equiv_eq' idp qed)
 
     definition equiv_eq_iso (A B : set) : (A ≃ B) = (A ≅ B) :=
     ua !equiv_equiv_iso
diff --git a/hott/algebra/category/groupoid.hlean b/hott/algebra/category/groupoid.hlean
index 4642a7d9a..03294e446 100644
--- a/hott/algebra/category/groupoid.hlean
+++ b/hott/algebra/category/groupoid.hlean
@@ -23,12 +23,13 @@ namespace category
   precategory.rec_on C groupoid.mk' H
 
   -- We can turn each group into a groupoid on the unit type
-  definition groupoid_of_group.{l} (A : Type.{l}) [G : group A] : groupoid.{0 l} unit :=
+  definition groupoid_of_group.{l} [constructor] (A : Type.{l}) [G : group A] :
+    groupoid.{0 l} unit :=
   begin
     fapply groupoid.mk, fapply precategory.mk,
       intros, exact A,
       intros, apply (@group.is_set_carrier A G),
-      intros [a, b, c, g, h], exact (@group.mul A G g h),
+      intros a b c g h, exact (@group.mul A G g h),
       intro a, exact (@group.one A G),
       intros, exact (@group.mul_assoc A G h g f)⁻¹,
       intros, exact (@group.one_mul A G f),
@@ -38,8 +39,7 @@ namespace category
         apply mul.right_inv,
   end
 
-  definition hom_group {A : Type} [G : groupoid A] (a : A) :
-    group (hom a a) :=
+  definition hom_group [constructor] {A : Type} [G : groupoid A] (a : A) : group (hom a a) :=
   begin
     fapply group.mk,
       intro f g, apply (comp f g),
@@ -64,15 +64,19 @@ namespace category
 
   attribute Groupoid.struct [instance] [coercion]
 
-  definition Groupoid.to_Precategory [coercion] [reducible] (C : Groupoid) : Precategory :=
+  definition Groupoid.to_Precategory [coercion] [reducible] [unfold 1] (C : Groupoid)
+    : Precategory :=
   Precategory.mk (Groupoid.carrier C) _
 
-  definition groupoid.Mk [reducible] := Groupoid.mk
-  definition groupoid.MK [reducible] (C : Precategory) (H : Π (a b : C) (f : a ⟶ b), is_iso f)
-    : Groupoid :=
+  attribute Groupoid._trans_of_to_Precategory_1 [unfold 1]
+
+  definition groupoid.Mk [reducible] [constructor] := Groupoid.mk
+  definition groupoid.MK [reducible] [constructor] (C : Precategory)
+    (H : Π (a b : C) (f : a ⟶ b), is_iso f) : Groupoid :=
   Groupoid.mk C (groupoid.mk C H)
 
-  definition Groupoid.eta (C : Groupoid) : Groupoid.mk C C = C :=
+  definition Groupoid.eta [unfold 1] (C : Groupoid) : Groupoid.mk C C = C :=
   Groupoid.rec (λob c, idp) C
 
+
 end category
diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean
index 962291e23..cec39ec31 100644
--- a/hott/algebra/category/iso.hlean
+++ b/hott/algebra/category/iso.hlean
@@ -383,3 +383,35 @@ namespace iso
   by rewrite [-comp_inverse_cancel_right r q, H, comp_inverse_cancel_right _ q]
   end
 end iso
+
+namespace iso
+
+  /- precomposition and postcomposition by an iso is an equivalence -/
+
+  definition is_equiv_postcompose [constructor] {ob : Type} [precategory ob] {a b c : ob}
+    (g : b ⟶ c) [is_iso g] : is_equiv (λ(f : a ⟶ b), g ∘ f) :=
+  begin
+    fapply adjointify,
+    { exact λf', g⁻¹ ∘ f'},
+    { intro f', apply comp_inverse_cancel_left},
+    { intro f, apply inverse_comp_cancel_left}
+  end
+
+  definition equiv_postcompose [constructor] {ob : Type} [precategory ob] {a b c : ob}
+    (g : b ⟶ c) [is_iso g] : (a ⟶ b) ≃ (a ⟶ c) :=
+  equiv.mk (λ(f : a ⟶ b), g ∘ f) (is_equiv_postcompose g)
+
+  definition is_equiv_precompose [constructor] {ob : Type} [precategory ob] {a b c : ob}
+    (f : a ⟶ b) [is_iso f] : is_equiv (λ(g : b ⟶ c), g ∘ f) :=
+  begin
+    fapply adjointify,
+    { exact λg', g' ∘ f⁻¹},
+    { intro g', apply comp_inverse_cancel_right},
+    { intro g, apply inverse_comp_cancel_right}
+  end
+
+  definition equiv_precompose [constructor] {ob : Type} [precategory ob] {a b c : ob}
+    (f : a ⟶ b) [is_iso f] : (b ⟶ c) ≃ (a ⟶ c) :=
+  equiv.mk (λ(g : b ⟶ c), g ∘ f) (is_equiv_precompose f)
+
+end iso
diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean
index 3048e6938..2aa3cc3d4 100644
--- a/hott/algebra/e_closure.hlean
+++ b/hott/algebra/e_closure.hlean
@@ -10,7 +10,7 @@ A more appropriate intuition is the type of words formed from the relation,
 
 import algebra.relation eq2 arity cubical.pathover2
 
-open eq equiv
+open eq equiv function
 
 inductive e_closure {A : Type} (R : A → A → Type) : A → A → Type :=
 | of_rel : Π{a a'} (r : R a a'), e_closure R a a'
@@ -58,22 +58,51 @@ section
       exact ap_con g (e_closure.elim e r) (e_closure.elim e r') ⬝ (IH₁ ◾ IH₂)
   end
 
+  definition ap_e_closure_elim_h_symm [unfold_full] {B C : Type} {f : A → B} {g : B → C}
+    {e : Π⦃a a' : A⦄, R a a' → f a = f a'}
+    {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
+    (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a') :
+    ap_e_closure_elim_h e p t⁻¹ʳ = ap_inv g (e_closure.elim e t) ⬝ (ap_e_closure_elim_h e p t)⁻² :=
+  by reflexivity
+
+  definition ap_e_closure_elim_h_trans [unfold_full] {B C : Type} {f : A → B} {g : B → C}
+    {e : Π⦃a a' : A⦄, R a a' → f a = f a'}
+    {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
+    (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a') (t' : T a' a'')
+    : ap_e_closure_elim_h e p (t ⬝r t') = ap_con g (e_closure.elim e t) (e_closure.elim e t') ⬝
+      (ap_e_closure_elim_h e p t ◾ ap_e_closure_elim_h e p t') :=
+  by reflexivity
+
   definition ap_e_closure_elim [unfold 10] {B C : Type} {f : A → B} (g : B → C)
     (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a')
     : ap g (e_closure.elim e t) = e_closure.elim (λa a' r, ap g (e r)) t :=
   ap_e_closure_elim_h e (λa a' s, idp) t
 
-  definition ap_e_closure_elim_inv [unfold_full] {B C : Type} {f : A → B} (g : B → C)
+  definition ap_e_closure_elim_symm [unfold_full] {B C : Type} {f : A → B} (g : B → C)
     (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a')
     : ap_e_closure_elim g e t⁻¹ʳ = ap_inv g (e_closure.elim e t) ⬝ (ap_e_closure_elim g e t)⁻² :=
   by reflexivity
 
-  definition ap_e_closure_elim_con [unfold_full] {B C : Type} {f : A → B} (g : B → C)
+  definition ap_e_closure_elim_trans [unfold_full] {B C : Type} {f : A → B} (g : B → C)
     (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') (t' : T a' a'')
     : ap_e_closure_elim g e (t ⬝r t') = ap_con g (e_closure.elim e t) (e_closure.elim e t') ⬝
       (ap_e_closure_elim g e t ◾ ap_e_closure_elim g e t') :=
   by reflexivity
 
+  definition e_closure_elim_eq [unfold 8] {f : A → B}
+    {e e' : Π⦃a a' : A⦄, R a a' → f a = f a'} (p : e ~3 e') (t : T a a')
+    : e_closure.elim e t = e_closure.elim e' t :=
+  begin
+    induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂,
+      apply p,
+      reflexivity,
+      exact IH⁻²,
+      exact IH₁ ◾ IH₂
+  end
+
+  -- TODO: formulate and prove this without using function extensionality,
+  -- and modify the proofs using this to also not use function extensionality
+  -- strategy: use `e_closure_elim_eq` instead of `ap ... (eq_of_homotopy3 p)`
   definition ap_e_closure_elim_h_eq {B C : Type} {f : A → B} {g : B → C}
     (e : Π⦃a a' : A⦄, R a a' → f a = f a')
     {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
@@ -116,9 +145,38 @@ section
     : square (ap (ap h) (ap_e_closure_elim g e t))
              (ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) t)
              (ap_compose h g (e_closure.elim e t))⁻¹
-             (ap_e_closure_elim h (λa a' r, ap g (e r)) t) :=
+             (ap_e_closure_elim   h (λa a' r, ap g (e r)) t) :=
   !ap_ap_e_closure_elim_h
 
+  definition ap_e_closure_elim_h_zigzag {B C D : Type} {f : A → B}
+    {g : B → C} (h : C → D)
+    (e : Π⦃a a' : A⦄, R a a' → f a = f a')
+    {e' : Π⦃a a' : A⦄, R a a' → h (g (f a)) = h (g (f a'))}
+    (p : Π⦃a a' : A⦄ (s : R a a'), ap (h ∘ g) (e s) = e' s) (t : T a a')
+    : ap_e_closure_elim   h (λa a' s, ap g (e s)) t ⬝
+     (ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) t)⁻¹ ⬝
+      ap_e_closure_elim_h e p t =
+      ap_e_closure_elim_h (λa a' s, ap g (e s)) (λa a' s, (ap_compose h g (e s))⁻¹ ⬝ p s) t :=
+  begin
+    refine whisker_right (eq_of_square (ap_ap_e_closure_elim g h e t)⁻¹ʰ)⁻¹ _ ⬝ _,
+    refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con, apply eq_of_square,
+    apply transpose,
+    -- the rest of the proof is almost the same as the proof of ap_ap_e_closure_elim[_h].
+    -- Is there a connection between these theorems?
+    induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂,
+    { esimp, apply square_of_eq, apply idp_con},
+    { induction pp, apply ids},
+    { rewrite [▸*,ap_con (ap h)],
+      refine (transpose !ap_compose_inv)⁻¹ᵛ ⬝h _,
+      rewrite [con_inv,inv_inv,-inv2_inv],
+      exact !ap_inv2 ⬝v square_inv2 IH},
+    { rewrite [▸*,ap_con (ap h)],
+      refine (transpose !ap_compose_con)⁻¹ᵛ ⬝h _,
+      rewrite [con_inv,inv_inv,con2_inv],
+      refine !ap_con2 ⬝v square_con2 IH₁ IH₂},
+
+  end
+
   definition is_equivalence_e_closure : is_equivalence T :=
   begin
     constructor,
@@ -127,23 +185,6 @@ section
       intro a a' a'' t t', exact t ⬝r t',
   end
 
-/-
-  definition e_closure.transport_left {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a')
-    (t : e_closure R a a') (p : a = a'')
-    : e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t :=
-  by induction p; exact !idp_con⁻¹
-
-  definition e_closure.transport_right {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a')
-    (t : e_closure R a a') (p : a' = a'')
-    : e_closure.elim e (p ▸ t) = e_closure.elim e t ⬝ (ap f p) :=
-  by induction p; reflexivity
-
-  definition e_closure.transport_lr {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a')
-    (t : e_closure R a a) (p : a = a')
-    : e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t ⬝ (ap f p) :=
-  by induction p; esimp; exact !idp_con⁻¹
--/
-
   /- dependent elimination -/
 
   variables {P : B → Type} {Q : C → Type} {f : A → B} {g : B → C} {f' : Π(a : A), P (f a)}
@@ -158,12 +199,12 @@ section
       exact IH₁ ⬝o IH₂
   end
 
-  definition elimo_inv [unfold_full] (p : Π⦃a a' : A⦄, R a a' → f a = f a')
+  definition elimo_symm [unfold_full] (p : Π⦃a a' : A⦄, R a a' → f a = f a')
     (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a') (t : T a a')
     : e_closure.elimo p po t⁻¹ʳ = (e_closure.elimo p po t)⁻¹ᵒ :=
   by reflexivity
 
-  definition elimo_con [unfold_full] (p : Π⦃a a' : A⦄, R a a' → f a = f a')
+  definition elimo_trans [unfold_full] (p : Π⦃a a' : A⦄, R a a' → f a = f a')
     (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a') (t : T a a') (t' : T a' a'')
     : e_closure.elimo p po (t ⬝r t') = e_closure.elimo p po t ⬝o e_closure.elimo p po t' :=
   by reflexivity
@@ -192,10 +233,10 @@ section
     induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂,
     { reflexivity},
     { induction pp; reflexivity},
-    { rewrite [+elimo_inv, ap_e_closure_elim_inv, IH, con_inv, change_path_con, ▸*, -inv2_inv,
+    { rewrite [+elimo_symm, ap_e_closure_elim_symm, IH, con_inv, change_path_con, ▸*, -inv2_inv,
                change_path_invo, pathover_of_pathover_ap_invo]},
-    { rewrite [+elimo_con, ap_e_closure_elim_con, IH₁, IH₂, con_inv, change_path_con, ▸*, con2_inv,
-               change_path_cono, pathover_of_pathover_ap_cono]},
+    { rewrite [+elimo_trans, ap_e_closure_elim_trans, IH₁, IH₂, con_inv, change_path_con, ▸*,
+               con2_inv, change_path_cono, pathover_of_pathover_ap_cono]},
   end
 
 end
diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean
index 04b24bc04..36f050eec 100644
--- a/hott/algebra/homotopy_group.hlean
+++ b/hott/algebra/homotopy_group.hlean
@@ -6,26 +6,26 @@ Authors: Floris van Doorn
 homotopy groups of a pointed space
 -/
 
-import .trunc_group .hott types.trunc
+import .trunc_group types.trunc .group_theory
 
 open nat eq pointed trunc is_trunc algebra
 
 namespace eq
 
-  definition phomotopy_group [constructor] (n : ℕ) (A : Type*) : Set* :=
+  definition phomotopy_group [reducible] [constructor] (n : ℕ) (A : Type*) : Set* :=
   ptrunc 0 (Ω[n] A)
 
   definition homotopy_group [reducible] (n : ℕ) (A : Type*) : Type :=
   phomotopy_group n A
 
-  notation `π*[`:95  n:0    `] `:0 A:95 := phomotopy_group n A
-  notation `π[`:95 n:0 `] `:0 A:95 := homotopy_group n A
+  notation `π*[`:95 n:0 `] `:0 := phomotopy_group n
+  notation `π[`:95  n:0 `] `:0 :=  homotopy_group n
 
-  definition group_homotopy_group [instance] [constructor] (n : ℕ) (A : Type*)
+  definition group_homotopy_group [instance] [constructor] [reducible] (n : ℕ) (A : Type*)
     : group (π[succ n] A) :=
   trunc_group concat inverse idp con.assoc idp_con con_idp con.left_inv
 
-  definition comm_group_homotopy_group [constructor] (n : ℕ) (A : Type*)
+  definition comm_group_homotopy_group [constructor] [reducible] (n : ℕ) (A : Type*)
     : comm_group (π[succ (succ n)] A) :=
   trunc_comm_group concat inverse idp con.assoc idp_con con_idp con.left_inv eckmann_hilton
 
@@ -43,7 +43,15 @@ namespace eq
   notation `πg[`:95  n:0 ` +1] `:0 A:95 := ghomotopy_group n A
   notation `πag[`:95 n:0 ` +2] `:0 A:95 := cghomotopy_group n A
 
-  prefix `π₁`:95 := fundamental_group
+  notation `π₁` := fundamental_group
+
+  definition tr_mul_tr {n : ℕ} {A : Type*} (p q : Ω[n + 1] A) :
+    tr p *[πg[n+1] A] tr q = tr (p ⬝ q) :=
+  by reflexivity
+
+  definition tr_mul_tr' {n : ℕ} {A : Type*} (p q : Ω[succ n] A)
+    : tr p *[π[succ n] A] tr q = tr (p ⬝ q) :=
+  idp
 
   definition phomotopy_group_pequiv [constructor] (n : ℕ) {A B : Type*} (H : A ≃* B)
     : π*[n] A ≃* π*[n] B :=
@@ -105,8 +113,8 @@ namespace eq
   definition homotopy_group_functor (n : ℕ) {A B : Type*} (f : A →* B) : π[n] A → π[n] B :=
   phomotopy_group_functor n f
 
-  notation `π→*[`:95 n:0 `] `:0 f:95 := phomotopy_group_functor n f
-  notation `π→[`:95  n:0 `] `:0 f:95 :=  homotopy_group_functor n f
+  notation `π→*[`:95 n:0 `] `:0 := phomotopy_group_functor n
+  notation `π→[`:95  n:0 `] `:0 :=  homotopy_group_functor n
 
   definition tinverse [constructor] {X : Type*} : π*[1] X →* π*[1] X :=
   ptrunc_functor 0 pinverse
@@ -132,7 +140,36 @@ namespace eq
     apply ap tr, apply apn_con
   end
 
+  open group function
 
+  /- some homomorphisms -/
 
+  definition is_homomorphism_cast_loop_space_succ_eq_in {A : Type*} (n : ℕ) :
+    is_homomorphism
+      (cast (ap (trunc 0 ∘ pointed.carrier) (loop_space_succ_eq_in A (succ n)))
+        : πg[n+1+1] A → πg[n+1] Ω A) :=
+  begin
+    intro g h, induction g with g, induction h with h,
+    xrewrite [tr_mul_tr, - + fn_cast_eq_cast_fn _ (λn, tr), tr_mul_tr, ↑cast, -tr_compose,
+              loop_space_succ_eq_in_concat, - + tr_compose],
+  end
+
+  definition is_homomorphism_inverse (A : Type*) (n : ℕ)
+    : is_homomorphism (λp, p⁻¹ : πag[n+2] A → πag[n+2] A) :=
+  begin
+    intro g h, rewrite mul.comm,
+    induction g with g, induction h with h,
+    exact ap tr !con_inv
+  end
+
+  definition homotopy_group_homomorphism [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
+    : πg[n+1] A →g πg[n+1] B :=
+  begin
+    fconstructor,
+    { exact phomotopy_group_functor (n+1) f},
+    { apply phomotopy_group_functor_mul}
+  end
+
+  notation `π→g[`:95  n:0 ` +1] `:0 f:95 := homotopy_group_homomorphism n f
 
 end eq
diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean
index ce8105ceb..a356a7066 100644
--- a/hott/algebra/ring.hlean
+++ b/hott/algebra/ring.hlean
@@ -61,6 +61,13 @@ section semiring
 
   theorem distrib_three_right (a b c d : A) : (a + b + c) * d = a * d + b * d + c * d :=
     by rewrite *right_distrib
+
+  theorem mul_two : a * 2 = a + a :=
+  by rewrite [-one_add_one_eq_two, left_distrib, +mul_one]
+
+  theorem two_mul : 2 * a = a + a :=
+  by rewrite [-one_add_one_eq_two, right_distrib, +one_mul]
+
 end semiring
 
 /- comm semiring -/
diff --git a/hott/eq2.hlean b/hott/eq2.hlean
index 556398361..ee86f6ec7 100644
--- a/hott/eq2.hlean
+++ b/hott/eq2.hlean
@@ -118,5 +118,13 @@ namespace eq
     con_tr idp q u = ap (λp, p ▸ u) (idp_con q) :=
   by induction q;reflexivity
 
+  definition transport_eq_Fl_idp_left {A B : Type} {a : A} {b : B} (f : A → B) (q : f a = b)
+    : transport_eq_Fl idp q = !idp_con⁻¹ :=
+  by induction q; reflexivity
+
+  definition whisker_left_idp_con_eq_assoc
+    {A : Type} {a₁ a₂ a₃ : A} (p : a₁ = a₂) (q : a₂ = a₃)
+    : whisker_left p (idp_con q)⁻¹ = con.assoc p idp q :=
+  by induction q; reflexivity
 
 end eq
diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean
index 482e8b2b5..1d29b0f1e 100644
--- a/hott/hit/pushout.hlean
+++ b/hott/hit/pushout.hlean
@@ -3,7 +3,7 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 
-Declaration of the pushout
+Declaration and properties of the pushout
 -/
 
 import .quotient types.sigma types.arrow_2
@@ -84,6 +84,11 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
     : transport (elim_type Pinl Pinr Pglue) (glue x) = Pglue x :=
   !elim_type_eq_of_rel_fn
 
+  theorem elim_type_glue_inv (Pinl : BL → Type) (Pinr : TR → Type)
+    (Pglue : Π(x : TL), Pinl (f x) ≃ Pinr (g x)) (x : TL)
+    : transport (elim_type Pinl Pinr Pglue) (glue x)⁻¹ = to_inv (Pglue x) :=
+  !elim_type_eq_of_rel_inv
+
   protected definition rec_prop {P : pushout → Type} [H : Πx, is_prop (P x)]
     (Pinl : Π(x : BL), P (inl x)) (Pinr : Π(x : TR), P (inr x)) (y : pushout) :=
   rec Pinl Pinr (λx, !is_prop.elimo) y
diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean
index 94968740c..1ba872cd7 100644
--- a/hott/hit/quotient.hlean
+++ b/hott/hit/quotient.hlean
@@ -58,6 +58,11 @@ namespace quotient
     : transport (quotient.elim_type Pc Pp) (eq_of_rel R H) = to_fun (Pp H) :=
   by rewrite [tr_eq_cast_ap_fn, ↑quotient.elim_type, elim_eq_of_rel];apply cast_ua_fn
 
+  theorem elim_type_eq_of_rel_inv (Pc : A → Type)
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') {a a' : A} (H : R a a')
+    : transport (quotient.elim_type Pc Pp) (eq_of_rel R H)⁻¹ = to_inv (Pp H) :=
+  by rewrite [tr_eq_cast_ap_fn, ↑quotient.elim_type, ap_inv, elim_eq_of_rel];apply cast_ua_inv_fn
+
   theorem elim_type_eq_of_rel.{u} (Pc : A → Type.{u})
     (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') {a a' : A} (H : R a a') (p : Pc a)
     : transport (quotient.elim_type Pc Pp) (eq_of_rel R H) p = to_fun (Pp H) p :=
diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean
index baafed5b9..f7da0347f 100644
--- a/hott/hit/two_quotient.hlean
+++ b/hott/hit/two_quotient.hlean
@@ -332,6 +332,7 @@ namespace simple_two_quotient
 end
 end simple_two_quotient
 
+export [unfold] simple_two_quotient
 attribute simple_two_quotient.j simple_two_quotient.incl0 [constructor]
 attribute simple_two_quotient.rec simple_two_quotient.elim [unfold 8] [recursor 8]
 --attribute simple_two_quotient.elim_type [unfold 9] -- TODO
@@ -370,8 +371,8 @@ namespace two_quotient
     { exact P0 a},
     { exact P1 s},
     { exact abstract [irreducible] begin induction q with a a' t t' q,
-      rewrite [elimo_con (simple_two_quotient.incl1 R Q2) P1,
-               elimo_inv (simple_two_quotient.incl1 R Q2) P1,
+      rewrite [elimo_trans (simple_two_quotient.incl1 R Q2) P1,
+               elimo_symm (simple_two_quotient.incl1 R Q2) P1,
                -whisker_right_eq_of_con_inv_eq_idp (simple_two_quotient.incl2 R Q2 (Qmk R q)),
                change_path_con],
       xrewrite [change_path_cono],
@@ -430,7 +431,7 @@ namespace two_quotient
     {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
     (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
     ⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (inclt t) = e_closure.elim P1 t :=
-  !elim_inclt
+  ap_e_closure_elim_h incl1 (elim_incl1 P2) t
 
   theorem elim_incl2 {P : Type} (P0 : A → P)
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
diff --git a/hott/homotopy/cylinder.hlean b/hott/homotopy/cylinder.hlean
index 410da225f..e53d551bf 100644
--- a/hott/homotopy/cylinder.hlean
+++ b/hott/homotopy/cylinder.hlean
@@ -8,13 +8,12 @@ Declaration of mapping cylinders
 
 import hit.quotient
 
-open quotient eq sum equiv
+open quotient eq sum equiv fiber
 
 namespace cylinder
 section
 
-universe u
-parameters {A B : Type.{u}} (f : A → B)
+  parameters {A B : Type} (f : A → B)
 
   local abbreviation C := B + A
   inductive cylinder_rel : C → C → Type :=
@@ -24,6 +23,7 @@ parameters {A B : Type.{u}} (f : A → B)
 
   definition cylinder := quotient cylinder_rel -- TODO: define this in root namespace
 
+  parameter {f}
   definition base (b : B) : cylinder :=
   class_of R (inl b)
 
@@ -93,3 +93,51 @@ attribute cylinder.rec cylinder.elim [unfold 8] [recursor 8]
 attribute cylinder.elim_type [unfold 7]
 attribute cylinder.rec_on cylinder.elim_on [unfold 5]
 attribute cylinder.elim_type_on [unfold 4]
+
+namespace cylinder
+  open sigma sigma.ops
+  variables {A B : Type} (f : A → B)
+
+  /- cylinder as a dependent family -/
+  definition pr1 [unfold 4] : cylinder f → B :=
+  cylinder.elim id f (λa, idp)
+
+  definition fcylinder : B → Type := fiber (pr1 f)
+
+  definition cylinder_equiv_sigma_fcylinder [constructor] : cylinder f ≃ Σb, fcylinder f b :=
+  !sigma_fiber_equiv⁻¹ᵉ
+
+  variable {f}
+  definition fbase (b : B) : fcylinder f b :=
+  fiber.mk (base b) idp
+
+  definition ftop (a : A) : fcylinder f (f a) :=
+  fiber.mk (top a) idp
+
+  definition fseg (a : A) : fbase (f a) = ftop a :=
+  fiber_eq (seg a) !elim_seg⁻¹
+
+--   set_option pp.notation false
+--   -- The induction principle for the dependent mapping cylinder (TODO)
+--   protected definition frec {P : Π(b), fcylinder f b → Type}
+--     (Pbase : Π(b : B), P _ (fbase b)) (Ptop : Π(a : A), P _ (ftop a))
+--     (Pseg : Π(a : A), Pbase (f a) =[fseg a] Ptop a) {b : B} (x : fcylinder f b) : P _ x :=
+--   begin
+--     cases x with x p, induction p,
+--     induction x: esimp,
+--     { apply Pbase},
+--     { apply Ptop},
+--     { esimp, --fapply fiber_pathover,
+--              --refine pathover_of_pathover_ap P (λx, fiber.mk x idp),
+
+-- exact sorry}
+--   end
+
+--   theorem frec_fseg {P : Π(b), fcylinder f b → Type}
+--     (Pbase : Π(b : B), P _ (fbase b)) (Ptop : Π(a : A), P _ (ftop a))
+--     (Pseg : Π(a : A), Pbase (f a) =[fseg a] Ptop a) (a : A)
+--     : apd (cylinder.frec Pbase Ptop Pseg) (fseg a) = Pseg a :=
+--   sorry
+
+
+end cylinder
diff --git a/hott/homotopy/hopf.hlean b/hott/homotopy/hopf.hlean
index d199ace9d..017ae94b3 100644
--- a/hott/homotopy/hopf.hlean
+++ b/hott/homotopy/hopf.hlean
@@ -69,14 +69,14 @@ section
     { fapply equiv.MK
              (λz : A × A, (z.1 * z.2, z.2))
              (λz : A × A, ((λx, x * z.2)⁻¹ z.1, z.2)),
-      { intro z, induction z with u v, esimp, 
+      { intro z, induction z with u v, esimp,
         exact prod_eq (right_inv (λx, x * v) u) idp },
       { intro z, induction z with a b, esimp,
         exact prod_eq (left_inv (λx, x * b) a) idp } },
-    { exact erfl },
-    { exact erfl },
-    { intro z, reflexivity },
-    { intro z, reflexivity }
+    { reflexivity },
+    { reflexivity },
+    { reflexivity },
+    { reflexivity }
   end
 end
 
diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean
index cfa080707..573b8d08b 100644
--- a/hott/homotopy/sphere.hlean
+++ b/hott/homotopy/sphere.hlean
@@ -67,7 +67,7 @@ namespace sphere_index
   | sp_refl : le a a
   | step : Π {b}, le a b → le a (b.+1)
 
-  infix `+1+`:65 := sphere_index.add_plus_one
+  infix ` +1+ `:65 := sphere_index.add_plus_one
 
   definition has_add_sphere_index [instance] [priority 2000] [reducible] : has_add ℕ₋₁ :=
   has_add.mk sphere_index.add
@@ -75,7 +75,7 @@ namespace sphere_index
   definition has_le_sphere_index [instance] : has_le ℕ₋₁ :=
   has_le.mk sphere_index.le
 
-  definition of_nat [coercion] [reducible] (n : nat) : ℕ₋₁ :=
+  definition of_nat [coercion] [reducible] (n : ℕ) : ℕ₋₁ :=
   (nat.rec_on n -1 (λ n k, k.+1)).+1
 
   definition sub_one [reducible] (n : ℕ) : ℕ₋₁ :=
diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean
index f2b491c76..228d705a6 100644
--- a/hott/homotopy/susp.hlean
+++ b/hott/homotopy/susp.hlean
@@ -69,6 +69,10 @@ namespace susp
     (a : A) : transport (susp.elim_type PN PS Pm) (merid a) = Pm a :=
   !elim_type_glue
 
+  theorem elim_type_merid_inv {A : Type} (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
+    (a : A) : transport (susp.elim_type PN PS Pm) (merid a)⁻¹ = to_inv (Pm a) :=
+  !elim_type_glue_inv
+
   protected definition merid_square {a a' : A} (p : a = a')
     : square (merid a) (merid a') idp idp :=
   by cases p; apply vrefl
@@ -198,12 +202,12 @@ namespace susp
 end susp
 
 open susp
-definition psusp [constructor] (X : Type) : pType :=
+definition psusp [constructor] (X : Type) : Type* :=
 pointed.mk' (susp X)
 
 namespace susp
   open pointed
-  variables {X Y Z : pType}
+  variables {X Y Z : Type*}
 
   definition psusp_functor (f : X →* Y) : psusp X →* psusp Y :=
   begin
@@ -234,7 +238,7 @@ namespace susp
 
   -- adjunction from Coq-HoTT
 
-  definition loop_susp_unit [constructor] (X : pType) : X →* Ω(psusp X) :=
+  definition loop_susp_unit [constructor] (X : Type*) : X →* Ω(psusp X) :=
   begin
     fconstructor,
     { intro x, exact merid x ⬝ (merid pt)⁻¹},
@@ -263,7 +267,7 @@ namespace susp
       xrewrite [idp_con_idp, -ap_compose (concat idp)]},
   end
 
-  definition loop_susp_counit [constructor] (X : pType) : psusp (Ω X) →* X :=
+  definition loop_susp_counit [constructor] (X : Type*) : psusp (Ω X) →* X :=
   begin
     fconstructor,
     { intro x, induction x, exact pt, exact pt, exact a},
@@ -284,7 +288,7 @@ namespace susp
     { reflexivity}
   end
 
-  definition loop_susp_counit_unit (X : pType)
+  definition loop_susp_counit_unit (X : Type*)
     : ap1 (loop_susp_counit X) ∘* loop_susp_unit (Ω X) ~* pid (Ω X) :=
   begin
     induction X with X x, fconstructor,
@@ -298,7 +302,7 @@ namespace susp
       xrewrite [ap_con_right_inv (susp.elim x x (λa, a)) (merid idp),idp_con_idp,-ap_compose]}
   end
 
-  definition loop_susp_unit_counit (X : pType)
+  definition loop_susp_unit_counit (X : Type*)
     : loop_susp_counit (psusp X) ∘* psusp_functor (loop_susp_unit X) ~* pid (psusp X) :=
   begin
     induction X with X x, fconstructor,
@@ -311,7 +315,7 @@ namespace susp
     { reflexivity}
   end
 
-  definition susp_adjoint_loop (X Y : pType) : map₊ (pointed.mk' (susp X)) Y ≃ map₊ X (Ω Y) :=
+  definition susp_adjoint_loop (X Y : Type*) : pointed.mk' (susp X) →* Y ≃ X →* Ω Y :=
   begin
     fapply equiv.MK,
     { intro f, exact ap1 f ∘* loop_susp_unit X},
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 18fba5ff1..7f283a1f1 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -276,6 +276,12 @@ namespace is_equiv
   !ap_eq_of_fn_eq_fn'
 
   end
+
+  -- This is inv_commute' for A ≡ unit
+  definition inv_commute1' {B C : Type} (f : B → C) [is_equiv f] (h : B → B) (h' : C → C)
+    (p : Π(b : B), f (h b) = h' (f b)) (c : C) : f⁻¹ (h' c) = h (f⁻¹ c) :=
+  eq_of_fn_eq_fn' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹)
+
 end is_equiv
 open is_equiv
 
@@ -310,9 +316,12 @@ namespace equiv
   definition to_left_inv [reducible] [unfold 3] (f : A ≃ B) (a : A) : f⁻¹ (f a) = a :=
   left_inv f a
 
-  protected definition refl [refl] [constructor] : A ≃ A :=
+  protected definition rfl [refl] [constructor] : A ≃ A :=
   equiv.mk id !is_equiv_id
 
+  protected definition refl [constructor] [reducible] (A : Type) : A ≃ A :=
+  @equiv.rfl A
+
   protected definition symm [symm] [constructor] (f : A ≃ B) : B ≃ A :=
   equiv.mk f⁻¹ !is_equiv_inv
 
@@ -322,7 +331,7 @@ namespace equiv
   infixl ` ⬝e `:75 := equiv.trans
   postfix `⁻¹ᵉ`:(max + 1) := equiv.symm
     -- notation for inverse which is not overloaded
-  abbreviation erfl [constructor] := @equiv.refl
+  abbreviation erfl [constructor] := @equiv.rfl
 
   definition to_inv_trans [reducible] [unfold_full] (f : A ≃ B) (g : B ≃ C)
     : to_inv (f ⬝e g) = to_fun (g⁻¹ᵉ ⬝e f⁻¹ᵉ) :=
@@ -395,6 +404,10 @@ namespace equiv
     {a : A} (b : B (g' a)) : f (h b) = h' (f b) :=
   fun_commute_of_inv_commute' @f @h @h' p b
 
+  definition inv_commute1 {B C : Type} (f : B ≃ C) (h : B → B) (h' : C → C)
+    (p : Π(b : B), f (h b) =   h' (f b)) (c : C) : f⁻¹ (h' c) = h (f⁻¹ c) :=
+  inv_commute1' (to_fun f) h h' p c
+
   end
 
   infixl ` ⬝pe `:75 := equiv_of_equiv_of_eq
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 6406a00b1..f47bec2f2 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -92,7 +92,6 @@ namespace eq
   definition inv_con_inv_left (p : y = x) (q : y = z) : (p⁻¹ ⬝ q)⁻¹ = q⁻¹ ⬝ p :=
   by induction q; induction p; reflexivity
 
-  -- universe metavariables
   definition inv_con_inv_right (p : x = y) (q : z = y) : (p ⬝ q⁻¹)⁻¹ = q ⬝ p⁻¹ :=
   by induction q; induction p; reflexivity
 
@@ -444,6 +443,14 @@ namespace eq
     p⁻¹ ▸ p ▸ z = z :=
   (con_tr p p⁻¹ z)⁻¹ ⬝ ap (λr, transport P r z) (con.right_inv p)
 
+  definition cast_cast_inv {A : Type} {P : A → Type} {x y : A} (p : x = y) (z : P y) :
+    cast (ap P p) (cast (ap P p⁻¹) z) = z :=
+  by induction p; reflexivity
+
+  definition cast_inv_cast {A : Type} {P : A → Type} {x y : A} (p : x = y) (z : P x) :
+    cast (ap P p⁻¹) (cast (ap P p) z) = z :=
+  by induction p; reflexivity
+
   definition con_con_tr {P : A → Type}
       {x y z w : A} (p : x = y) (q : y = z) (r : z = w) (u : P x) :
     ap (λe, e ▸ u) (con.assoc' p q r) ⬝ (con_tr (p ⬝ q) r u) ⬝
@@ -515,6 +522,10 @@ namespace eq
     f y (p ▸ z) = p ▸ f x z :=
   by induction p; reflexivity
 
+  definition fn_cast_eq_cast_fn {A : Type} {P Q : A → Type} {x y : A} (p : x = y)
+    (f : Πx, P x → Q x) (z : P x) : f y (cast (ap P p) z) = cast (ap Q p) (f x z) :=
+  by induction p; reflexivity
+
   /- Transporting in particular fibrations -/
 
   /-
diff --git a/hott/init/pointed.hlean b/hott/init/pointed.hlean
index dce7158f6..f7c7ea810 100644
--- a/hott/init/pointed.hlean
+++ b/hott/init/pointed.hlean
@@ -40,6 +40,11 @@ open pointed
 section
   universe variable u
   structure ptrunctype (n : trunc_index) extends trunctype.{u} n, pType.{u}
+
+  definition is_trunc_ptrunctype [instance] {n : ℕ₋₂} (X : ptrunctype n)
+    : is_trunc n (ptrunctype.to_pType X) :=
+  trunctype.struct X
+
 end
 
 notation n `-Type*` := ptrunctype n
diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean
index 22aa941da..6ba8c5756 100644
--- a/hott/init/ua.hlean
+++ b/hott/init/ua.hlean
@@ -22,7 +22,7 @@ section
   equiv.mk _ (is_equiv_cast_of_eq H)
 
   definition equiv_of_eq_refl [reducible] [unfold_full] (A : Type)
-    : equiv_of_eq (refl A) = equiv.refl :=
+    : equiv_of_eq (refl A) = equiv.refl A :=
   idp
 
 
@@ -75,7 +75,7 @@ namespace equiv
 
   -- a variant where we immediately recurse on the equality in the new goal
   definition rec_on_ua_idp [recursor] {A : Type} {P : Π{B}, A ≃ B → Type} {B : Type}
-    (f : A ≃ B) (H : P equiv.refl) : P f :=
+    (f : A ≃ B) (H : P equiv.rfl) : P f :=
   rec_on_ua f (λq, eq.rec_on q H)
 
   -- a variant where (equiv_of_eq (ua f)) will be replaced by f in the new goal
@@ -85,7 +85,7 @@ namespace equiv
 
   -- a variant where we do both
   definition rec_on_ua_idp' {A : Type} {P : Π{B}, A ≃ B → A = B → Type} {B : Type}
-    (f : A ≃ B) (H : P equiv.refl idp) : P f (ua f) :=
+    (f : A ≃ B) (H : P equiv.rfl idp) : P f (ua f) :=
   rec_on_ua' f (λq, eq.rec_on q H)
 
   definition ua_refl (A : Type) : ua erfl = idpath A :=
diff --git a/hott/types/arrow.hlean b/hott/types/arrow.hlean
index 91a892eb1..a496dba53 100644
--- a/hott/types/arrow.hlean
+++ b/hott/types/arrow.hlean
@@ -38,14 +38,14 @@ namespace pi
 
   variable (A)
   definition arrow_equiv_arrow_right [constructor] (f1 : B ≃ B') : (A → B) ≃ (A → B') :=
-  arrow_equiv_arrow_rev equiv.refl f1
+  arrow_equiv_arrow_rev equiv.rfl f1
 
   variables {A} (B)
   definition arrow_equiv_arrow_left_rev [constructor] (f0 : A' ≃ A) : (A → B) ≃ (A' → B) :=
-  arrow_equiv_arrow_rev f0 equiv.refl
+  arrow_equiv_arrow_rev f0 equiv.rfl
 
   definition arrow_equiv_arrow_left [constructor] (f0 : A ≃ A') : (A → B) ≃ (A' → B) :=
-  arrow_equiv_arrow f0 equiv.refl
+  arrow_equiv_arrow f0 equiv.rfl
 
   variables {B}
   definition arrow_equiv_arrow_right' [constructor] (f1 : A → (B ≃ B')) : (A → B) ≃ (A → B') :=
diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean
index ec8c91372..af916be3b 100644
--- a/hott/types/eq.hlean
+++ b/hott/types/eq.hlean
@@ -456,13 +456,13 @@ namespace eq
     parameters {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a))
       (p : (center (Σa, code a)).1 = a₀)
     include p
-    definition encode {a : A} (q : a₀ = a) : code a :=
+    protected definition encode {a : A} (q : a₀ = a) : code a :=
     (p ⬝ q) ▸ (center (Σa, code a)).2
 
-    definition decode' {a : A} (c : code a) : a₀ = a :=
+    protected definition decode' {a : A} (c : code a) : a₀ = a :=
     (is_prop.elim ⟨a₀, encode idp⟩ ⟨a, c⟩)..1
 
-    definition decode {a : A} (c : code a) : a₀ = a :=
+    protected definition decode {a : A} (c : code a) : a₀ = a :=
     (decode' (encode idp))⁻¹ ⬝ decode' c
 
     definition total_space_method (a : A) : (a₀ = a) ≃ code a :=
diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean
index 149cfe4f5..725e2cfbe 100644
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@@ -208,17 +208,17 @@ namespace equiv
       : equiv.mk f H = equiv.mk f' H' :=
   apd011 equiv.mk p !is_prop.elim
 
-  definition equiv_eq {f f' : A ≃ B} (p : to_fun f = to_fun f') : f = f' :=
+  definition equiv_eq' {f f' : A ≃ B} (p : to_fun f = to_fun f') : f = f' :=
   by (cases f; cases f'; apply (equiv_mk_eq p))
 
-  definition equiv_eq' {f f' : A ≃ B} (p : to_fun f ~ to_fun f') : f = f' :=
-  by apply equiv_eq;apply eq_of_homotopy p
+  definition equiv_eq {f f' : A ≃ B} (p : to_fun f ~ to_fun f') : f = f' :=
+  by apply equiv_eq'; apply eq_of_homotopy p
 
   definition trans_symm (f : A ≃ B) (g : B ≃ C) : (f ⬝e g)⁻¹ᵉ = g⁻¹ᵉ ⬝e f⁻¹ᵉ :> (C ≃ A) :=
-  equiv_eq idp
+  equiv_eq' idp
 
   definition symm_symm (f : A ≃ B) : f⁻¹ᵉ⁻¹ᵉ = f :> (A ≃ B) :=
-  equiv_eq idp
+  equiv_eq' idp
 
   protected definition equiv.sigma_char [constructor]
     (A B : Type) : (A ≃ B) ≃ Σ(f : A → B), is_equiv f :=
@@ -235,7 +235,7 @@ namespace equiv
     (f = f') ≃ (to_fun !equiv.sigma_char f = to_fun !equiv.sigma_char f')
                 : eq_equiv_fn_eq (to_fun !equiv.sigma_char)
          ... ≃ ((to_fun !equiv.sigma_char f).1 = (to_fun !equiv.sigma_char f').1 ) : equiv_subtype
-         ... ≃ (to_fun f = to_fun f') : equiv.refl
+         ... ≃ (to_fun f = to_fun f') : equiv.rfl
 
   definition is_equiv_ap_to_fun (f f' : A ≃ B)
     : is_equiv (ap to_fun : f = f' → to_fun f = to_fun f') :=
@@ -276,4 +276,19 @@ namespace equiv
   [HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A ≃ B) :=
   by cases n; apply !is_contr_equiv; apply !is_trunc_succ_equiv
 
+  definition eq_of_fn_eq_fn'_idp {A B : Type} (f : A → B) [is_equiv f] (x : A)
+    : eq_of_fn_eq_fn' f (idpath (f x)) = idpath x :=
+  !con.left_inv
+
+  definition eq_of_fn_eq_fn'_con {A B : Type} (f : A → B) [is_equiv f] {x y z : A}
+    (p : f x = f y) (q : f y = f z)
+    : eq_of_fn_eq_fn' f (p ⬝ q) = eq_of_fn_eq_fn' f p ⬝ eq_of_fn_eq_fn' f q :=
+  begin
+    unfold eq_of_fn_eq_fn',
+    refine _ ⬝ !con.assoc, apply whisker_right,
+    refine _ ⬝ !con.assoc⁻¹ ⬝ !con.assoc⁻¹, apply whisker_left,
+    refine !ap_con ⬝ _, apply whisker_left,
+    refine !con_inv_cancel_left⁻¹
+  end
+
 end equiv
diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean
index 700602e7b..e595d7b5e 100644
--- a/hott/types/fiber.hlean
+++ b/hott/types/fiber.hlean
@@ -7,7 +7,7 @@ Ported from Coq HoTT
 Theorems about fibers
 -/
 
-import .sigma .eq .pi
+import .sigma .eq .pi cubical.squareover
 open equiv sigma sigma.ops eq pi
 
 structure fiber {A B : Type} (f : A → B) (b : B) :=
@@ -43,6 +43,20 @@ namespace fiber
     (q : point_eq x = ap f p ⬝ point_eq y) : x = y :=
   to_inv !fiber_eq_equiv ⟨p, q⟩
 
+  definition fiber_pathover {X : Type} {A B : X → Type} {x₁ x₂ : X} {p : x₁ = x₂}
+    {f : Πx, A x → B x} {b : Πx, B x} {v₁ : fiber (f x₁) (b x₁)} {v₂ : fiber (f x₂) (b x₂)}
+    (q : point v₁ =[p] point v₂)
+    (r : squareover B hrfl (pathover_idp_of_eq (point_eq v₁)) (pathover_idp_of_eq (point_eq v₂))
+                           (apo f q) (apd b p))
+    : v₁ =[p] v₂ :=
+  begin
+    apply pathover_of_fn_pathover_fn (λa, !fiber.sigma_char), esimp,
+    fapply sigma_pathover: esimp,
+    { exact q},
+    { induction v₁ with a₁ p₁, induction v₂ with a₂ p₂, esimp at *, induction q, esimp at *,
+      apply pathover_idp_of_eq, apply eq_of_vdeg_square, apply square_of_squareover_ids r}
+  end
+
   open is_trunc
   definition fiber_pr1 (B : A → Type) (a : A) : fiber (pr1 : (Σa, B a) → A) a ≃ B a :=
   calc
diff --git a/hott/types/int/hott.hlean b/hott/types/int/hott.hlean
index c2a7cb8c4..36ff46209 100644
--- a/hott/types/int/hott.hlean
+++ b/hott/types/int/hott.hlean
@@ -14,7 +14,7 @@ namespace int
 
   section
   open algebra
-  definition group_integers : Group :=
+  definition group_integers [constructor] : Group :=
   Group.mk ℤ (group_of_add_group _)
 
   notation `gℤ` := group_integers
diff --git a/hott/types/lift.hlean b/hott/types/lift.hlean
index 86f90da02..fc16a6a29 100644
--- a/hott/types/lift.hlean
+++ b/hott/types/lift.hlean
@@ -73,7 +73,7 @@ namespace lift
   equiv.mk _ (is_equiv_lift_functor f)
 
   definition lift_equiv_lift_refl (A : Type) : lift_equiv_lift (erfl : A ≃ A) = erfl :=
-  by apply equiv_eq'; intro z; induction z with a; reflexivity
+  by apply equiv_eq; intro z; induction z with a; reflexivity
 
   definition lift_inv_functor [unfold_full] (a : A) : A' :=
   down (g (up a))
@@ -119,7 +119,7 @@ namespace lift
              intro f, apply equiv_eq, reflexivity
            end end
            abstract begin
-             intro g, apply equiv_eq, esimp, apply eq_of_homotopy, intro z,
+             intro g, apply equiv_eq', esimp, apply eq_of_homotopy, intro z,
              induction z with a, esimp, apply lift.eta
            end end
 
@@ -134,12 +134,12 @@ namespace lift
       exact _,
     { intro p, induction p,
       esimp [lift_eq_lift_equiv,equiv.trans,equiv.symm,eq_equiv_equiv],
-      rewrite [equiv_of_eq_refl,lift_equiv_lift_refl],
+      rewrite [equiv_of_eq_refl, lift_equiv_lift_refl],
       apply ua_refl}
   end
 
   definition plift [constructor] (A : pType.{u}) : pType.{max u v} :=
-  pType.mk (lift A) (up pt)
+  pointed.MK (lift A) (up pt)
 
   definition plift_functor [constructor] {A B : Type*} (f : A →* B) : plift A →* plift B :=
   pmap.mk (lift_functor f) (ap up (respect_pt f))
diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean
index 19dd30710..1e35829c9 100644
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@@ -176,7 +176,7 @@ namespace pi
     (f : Π(b : B a), C ⟨a, b⟩) (g : Π(b' : B a'), C ⟨a', b'⟩) :
     (Π(b : B a), (sigma_eq p !pathover_tr) ▸ (f b) = g (p ▸ b)) ≃
     (Π(b : B a), p ▸D (f b) = g (p ▸ b)) :=
-  eq.rec_on p (λg, !equiv.refl) g
+  eq.rec_on p (λg, !equiv.rfl) g
   end
 
   /- Functorial action -/
@@ -234,7 +234,7 @@ namespace pi
 
   definition pi_equiv_pi_right [constructor] {P Q : A → Type} (g : Πa, P a ≃ Q a)
     : (Πa, P a) ≃ (Πa, Q a) :=
-  pi_equiv_pi equiv.refl g
+  pi_equiv_pi equiv.rfl g
 
   /- Equivalence if one of the types is contractible -/
 
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index ccb68c5da..f2c218b0d 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -318,7 +318,7 @@ namespace pointed
   definition apn_succ [unfold_full] (n : ℕ) (f : map₊ A B) : Ω→[n + 1] f = ap1 (Ω→[n] f) := idp
 
   definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B :=
-  proof pmap.mk (cast (ap pType.carrier p)) (by induction p; reflexivity) qed
+  pmap.mk (cast (ap pType.carrier p)) (by induction p; reflexivity)
 
   definition pinverse [constructor] {X : Type*} : Ω X →* Ω X :=
   pmap.mk eq.inverse idp
@@ -439,6 +439,9 @@ namespace pointed
     : f ~* h :=
   phomotopy_of_eq p ⬝* q
 
+  infix ` ⬝*p `:75 := pconcat_eq
+  infix ` ⬝p* `:75 := eq_pconcat
+
   definition pwhisker_left [constructor] (h : B →* C) (p : f ~* g) : h ∘* f ~* h ∘* g :=
   phomotopy.mk (λa, ap h (p a))
     abstract begin
@@ -508,8 +511,12 @@ namespace pointed
   theorem apn_inv (n : ℕ)  (f : A →* B) (p : Ω[n+1] A) : apn (n+1) f p⁻¹ = (apn (n+1) f p)⁻¹ :=
   by rewrite [+apn_succ, ap1_inv]
 
-  infix ` ⬝*p `:75 := pconcat_eq
-  infix ` ⬝p* `:75 := eq_pconcat
+  definition pinverse_pinverse (A : Type*) : pinverse ∘* pinverse ~* pid (Ω A) :=
+  begin
+    fapply phomotopy.mk,
+    { apply inv_inv},
+    { reflexivity}
+  end
 
   /- pointed equivalences -/
 
@@ -529,6 +536,10 @@ namespace pointed
   definition to_pinv [constructor] (f : A ≃* B) : B →* A :=
   pmap.mk f⁻¹ ((ap f⁻¹ (respect_pt f))⁻¹ ⬝ left_inv f pt)
 
+  definition to_pmap_pequiv_of_pmap {A B : Type*} (f : A →* B) (H : is_equiv f)
+    : pequiv.to_pmap (pequiv_of_pmap f H) = f :=
+  by cases f; reflexivity
+
   /-
      A version of pequiv.MK with stronger conditions.
      The advantage of defining a pointed equivalence with this definition is that there is a
@@ -570,11 +581,15 @@ namespace pointed
   pequiv_of_pmap (to_pinv f) !is_equiv_inv
 
   protected definition pequiv.trans [trans] (f : A ≃* B) (g : B ≃* C) : A ≃* C :=
-  pequiv_of_pmap (pcompose g f) !is_equiv_compose
+  pequiv_of_pmap (g ∘* f) !is_equiv_compose
 
   postfix `⁻¹ᵉ*`:(max + 1) := pequiv.symm
   infix ` ⬝e* `:75 := pequiv.trans
 
+  definition to_pmap_pequiv_trans {A B C : Type*} (f : A ≃* B) (g : B ≃* C)
+    : pequiv.to_pmap (f ⬝e* g) = g ∘* f :=
+  !to_pmap_pequiv_of_pmap
+
   definition pequiv_change_fun [constructor] (f : A ≃* B) (f' : A →* B) (Heq : f ~ f') : A ≃* B :=
   pequiv_of_pmap f' (is_equiv.homotopy_closed f Heq)
 
@@ -736,14 +751,14 @@ namespace pointed
   ap1_con (loopn_pequiv_loopn n f) p q
 
   definition loopn_pequiv_loopn_rfl (n : ℕ) (A : Type*) :
-    loopn_pequiv_loopn n (@pequiv.refl A) = @pequiv.refl (Ω[n] A) :=
+    loopn_pequiv_loopn n (pequiv.refl A) = pequiv.refl (Ω[n] A) :=
   begin
     apply pequiv_eq, apply eq_of_phomotopy,
     exact !to_pmap_loopn_pequiv_loopn ⬝* apn_pid n,
   end
 
   definition loop_pequiv_loop_rfl (A : Type*) :
-    loop_pequiv_loop (@pequiv.refl A) = @pequiv.refl (Ω A) :=
+    loop_pequiv_loop (pequiv.refl A) = pequiv.refl (Ω A) :=
   loopn_pequiv_loopn_rfl 1 A
 
   definition pmap_functor [constructor] {A A' B B' : Type*} (f : A' →* A) (g : B →* B') :
@@ -755,6 +770,9 @@ namespace pointed
       { rewrite [▸*, ap_constant], apply idp_con}
     end end
 
+  definition pequiv_pinverse (A : Type*) : Ω A ≃* Ω A :=
+  pequiv_of_pmap pinverse !is_equiv_eq_inverse
+
 /- -- TODO
   definition pmap_pequiv_pmap {A A' B B' : Type*} (f : A ≃* A') (g : B ≃* B') :
     ppmap A B ≃* ppmap A' B' :=
diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean
index 81b88c520..8f3288a5e 100644
--- a/hott/types/prod.hlean
+++ b/hott/types/prod.hlean
@@ -155,10 +155,10 @@ namespace prod
   equiv.mk (prod_functor f g) _
 
   definition prod_equiv_prod_left [constructor] (g : B ≃ B') : A × B ≃ A × B' :=
-  prod_equiv_prod equiv.refl g
+  prod_equiv_prod equiv.rfl g
 
   definition prod_equiv_prod_right [constructor] (f : A ≃ A') : A × B ≃ A' × B :=
-  prod_equiv_prod f equiv.refl
+  prod_equiv_prod f equiv.rfl
 
   /- Symmetry -/
 
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index b13912ad5..8b449d179 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -73,7 +73,7 @@ namespace sigma
 
   /- the uncurried version of sigma_eq. We will prove that this is an equivalence -/
 
-  definition sigma_eq_unc : Π (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2), u = v
+  definition sigma_eq_unc [unfold 5] : Π (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2), u = v
   | sigma_eq_unc ⟨pq₁, pq₂⟩ := sigma_eq pq₁ pq₂
 
   definition dpair_sigma_eq_unc : Π (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2),
@@ -96,14 +96,15 @@ namespace sigma
       : transport (λx, B' x.1) (@sigma_eq_unc A B u v pq) = transport B' pq.1 :=
   destruct pq tr_pr1_sigma_eq
 
-  definition is_equiv_sigma_eq [instance] (u v : Σa, B a)
+  definition is_equiv_sigma_eq [instance] [constructor] (u v : Σa, B a)
       : is_equiv (@sigma_eq_unc A B u v) :=
   adjointify sigma_eq_unc
              (λp, ⟨p..1, p..2⟩)
              sigma_eq_eta_unc
              dpair_sigma_eq_unc
 
-  definition sigma_eq_equiv (u v : Σa, B a) : (u = v) ≃ (Σ(p : u.1 = v.1),  u.2 =[p] v.2) :=
+  definition sigma_eq_equiv [constructor] (u v : Σa, B a)
+    : (u = v) ≃ (Σ(p : u.1 = v.1),  u.2 =[p] v.2) :=
   (equiv.mk sigma_eq_unc _)⁻¹ᵉ
 
   definition dpair_eq_dpair_con (p1 : a  = a' ) (q1 : b  =[p1] b' )
@@ -243,7 +244,7 @@ namespace sigma
 
   definition sigma_equiv_sigma_right [constructor] {B' : A → Type} (Hg : Π a, B a ≃ B' a)
     : (Σa, B a) ≃ Σa, B' a :=
-  sigma_equiv_sigma equiv.refl Hg
+  sigma_equiv_sigma equiv.rfl Hg
 
   definition sigma_equiv_sigma_left [constructor] (Hf : A ≃ A') :
       (Σa, B a) ≃ (Σa', B (to_inv Hf a')) :=
@@ -307,7 +308,7 @@ namespace sigma
   calc
     (Σa a', C (a, a')) ≃ Σu, C u          : assoc_equiv_prod
                    ... ≃ Σv, C (flip v)   : sigma_equiv_sigma !prod_comm_equiv
-                                              (λu, prod.destruct u (λa a', equiv.refl))
+                                              (λu, prod.destruct u (λa a', equiv.rfl))
                    ... ≃ Σa' a, C (a, a') : assoc_equiv_prod
 
   definition sigma_comm_equiv [constructor] (C : A → A' → Type)
@@ -447,15 +448,17 @@ namespace sigma
   notation [parsing_only] `{` binder `|` r:(scoped:1 P, subtype P) `}` := r
 
   /- To prove equality in a subtype, we only need equality of the first component. -/
-  definition subtype_eq [H : Πa, is_prop (B a)] {u v : {a | B a}} : u.1 = v.1 → u = v :=
+  definition subtype_eq [unfold_full] [H : Πa, is_prop (B a)] {u v : {a | B a}} :
+    u.1 = v.1 → u = v :=
   sigma_eq_unc ∘ inv pr1
 
-  definition is_equiv_subtype_eq [H : Πa, is_prop (B a)] (u v : {a | B a})
+  definition is_equiv_subtype_eq [constructor] [H : Πa, is_prop (B a)] (u v : {a | B a})
       : is_equiv (subtype_eq : u.1 = v.1 → u = v) :=
   !is_equiv_compose
   local attribute is_equiv_subtype_eq [instance]
 
-  definition equiv_subtype [H : Πa, is_prop (B a)] (u v : {a | B a}) : (u.1 = v.1) ≃ (u = v) :=
+  definition equiv_subtype [constructor] [H : Πa, is_prop (B a)] (u v : {a | B a}) :
+    (u.1 = v.1) ≃ (u = v) :=
   equiv.mk !subtype_eq _
 
   definition subtype_eq_inv {A : Type} {B : A → Type} [H : Πa, is_prop (B a)] (u v : Σa, B a)
diff --git a/hott/types/sum.hlean b/hott/types/sum.hlean
index 652f5a290..91365b1f5 100644
--- a/hott/types/sum.hlean
+++ b/hott/types/sum.hlean
@@ -137,10 +137,10 @@ namespace sum
   equiv.mk _ (is_equiv_sum_functor f g)
 
   definition sum_equiv_sum_left [constructor] (g : B ≃ B') : A + B ≃ A + B' :=
-  sum_equiv_sum equiv.refl g
+  sum_equiv_sum equiv.rfl g
 
   definition sum_equiv_sum_right [constructor] (f : A ≃ A') : A + B ≃ A' + B :=
-  sum_equiv_sum f equiv.refl
+  sum_equiv_sum f equiv.rfl
 
   definition flip [unfold 3] : A + B → B + A
   | flip (inl a) := inr a
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index 048defcca..0ebf33c30 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -298,6 +298,48 @@ namespace is_trunc
       { apply minus_one_le_succ}}
   end
 
+  /- univalence for truncated types -/
+  definition teq_equiv_equiv {n : ℕ₋₂} {A B : n-Type} : (A = B) ≃ (A ≃ B) :=
+  trunctype_eq_equiv n A B ⬝e eq_equiv_equiv A B
+
+  definition tua {n : ℕ₋₂} {A B : n-Type} (f : A ≃ B) : A = B :=
+  (trunctype_eq_equiv n A B)⁻¹ᶠ (ua f)
+
+  definition tua_refl {n : ℕ₋₂} (A : n-Type) : tua (@erfl A) = idp :=
+  begin
+    refine ap (trunctype_eq_equiv n A A)⁻¹ᶠ (ua_refl A) ⬝ _,
+    esimp, refine ap (eq_of_fn_eq_fn _) _ ⬝ !eq_of_fn_eq_fn'_idp ,
+    esimp, apply ap (dpair_eq_dpair idp), apply is_prop.elim
+  end
+
+  definition tua_trans {n : ℕ₋₂} {A B C : n-Type} (f : A ≃ B) (g : B ≃ C)
+    : tua (f ⬝e g) = tua f ⬝ tua g :=
+  begin
+    refine ap (trunctype_eq_equiv n A C)⁻¹ᶠ (ua_trans f g) ⬝ _,
+    esimp, refine ap (eq_of_fn_eq_fn _) _ ⬝ !eq_of_fn_eq_fn'_con,
+    refine _ ⬝ !dpair_eq_dpair_con,
+    apply ap (dpair_eq_dpair _), apply is_prop.elim
+  end
+
+  definition tua_symm {n : ℕ₋₂} {A B : n-Type} (f : A ≃ B) : tua f⁻¹ᵉ = (tua f)⁻¹ :=
+  begin
+    apply eq_inv_of_con_eq_idp',
+    refine !tua_trans⁻¹ ⬝ _,
+    refine ap tua _ ⬝ !tua_refl,
+    apply equiv_eq, exact to_right_inv f
+  end
+
+  definition tcast [unfold 4] {n : ℕ₋₂} {A B : n-Type} (p : A = B) (a : A) : B :=
+  cast (ap trunctype.carrier p) a
+
+  theorem tcast_tua_fn {n : ℕ₋₂} {A B : n-Type} (f : A ≃ B) : tcast (tua f) = to_fun f :=
+  begin
+    cases A with A HA, cases B with B HB, esimp at *,
+    induction f using rec_on_ua_idp, esimp,
+    have HA = HB, from !is_prop.elim, cases this,
+    exact ap tcast !tua_refl
+  end
+
   /- theorems about decidable equality and axiom K -/
   theorem is_set_of_axiom_K {A : Type} (K : Π{a : A} (p : a = a), p = idp) : is_set A :=
   is_set.mk _ (λa b p q, eq.rec K q p)
diff --git a/hott/types/univ.hlean b/hott/types/univ.hlean
index f60e2fdc0..4734bfcf6 100644
--- a/hott/types/univ.hlean
+++ b/hott/types/univ.hlean
@@ -120,7 +120,7 @@ namespace univ
                                                    (λb, !sigma_assoc_equiv⁻¹ᵉ)
       ... ≃ Σb (Y : Type*), Y = fiber f b      : sigma_equiv_sigma_right
                                      (λb, sigma_equiv_sigma (pType.sigma_char)⁻¹ᵉ
-                                                            (λv, sigma.rec_on v (λx y, equiv.refl)))
+                                                            (λv, sigma.rec_on v (λx y, equiv.rfl)))
       ... ≃ Σ(Y : Type*) b, Y = fiber f b      : sigma_comm_equiv
       ... ≃ pullback pType.carrier (fiber f) : !pullback.sigma_char⁻¹ᵉ
         )
diff --git a/library/theories/move.lean b/library/theories/move.lean
index b2d468368..eafd096cc 100644
--- a/library/theories/move.lean
+++ b/library/theories/move.lean
@@ -42,9 +42,18 @@ quot.exact (by rewrite quot.mk_repr_eq)
 
 end quot
 
-
 -- move to data.set.basic
 
+-- move to algebra.ring
+
+theorem mul_two {A : Type} [semiring A] (a : A) : a * 2 = a + a :=
+by rewrite [-one_add_one_eq_two, left_distrib, +mul_one]
+
+theorem two_mul {A : Type} [semiring A] (a : A) : 2 * a = a + a :=
+by rewrite [-one_add_one_eq_two, right_distrib, +one_mul]
+
+-- move to data.set
+
 namespace set
 open function