diff --git a/hott/algebra/precategory/nat_trans.hlean b/hott/algebra/precategory/nat_trans.hlean
index 527ad731e..298f483b8 100644
--- a/hott/algebra/precategory/nat_trans.hlean
+++ b/hott/algebra/precategory/nat_trans.hlean
@@ -25,11 +25,11 @@ namespace nat_trans
     (λ a, η a ∘ θ a)
     (λ a b f,
       calc
-        H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : assoc
-                      ... = (η b ∘ G f) ∘ θ a : naturality η f
-                      ... = η b ∘ (G f ∘ θ a) : assoc
-                      ... = η b ∘ (θ b ∘ F f) : naturality θ f
-                      ... = (η b ∘ θ b) ∘ F f : assoc)
+        H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : by rewrite assoc
+                      ... = (η b ∘ G f) ∘ θ a : by rewrite naturality
+                      ... = η b ∘ (G f ∘ θ a) : by rewrite assoc
+                      ... = η b ∘ (θ b ∘ F f) : by rewrite naturality
+                      ... = (η b ∘ θ b) ∘ F f : by rewrite assoc)
 
   infixr `∘n`:60 := compose
 
diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean
index 84efb7eaf..c43172f79 100644
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@@ -23,13 +23,13 @@ namespace is_equiv
     is_contr.mk
       (fiber.mk (f⁻¹ b) (retr f b))
       (λz, fiber.rec_on z (λa p, fiber.eq_mk ((ap f⁻¹ p)⁻¹ ⬝ sect f a) (calc
-        retr f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ retr f b) : inv_con_cancel_left
-             ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (retr f (f a) ⬝ p) : by rewrite ap_con_eq_con
-             ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (sect f a) ⬝ p) : by rewrite adj
-             ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (sect f a) ⬝ p : con.assoc
-             ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (sect f a) ⬝ p : by rewrite ap_compose
-             ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (sect f a) ⬝ p : by rewrite ap_inv
-             ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ sect f a) ⬝ p : by rewrite ap_con)))
+        retr f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ retr f b) : by rewrite inv_con_cancel_left
+             ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (retr f (f a) ⬝ p)       : by rewrite ap_con_eq_con
+             ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (sect f a) ⬝ p)    : by rewrite adj
+             ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (sect f a) ⬝ p      : by rewrite con.assoc
+             ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (sect f a) ⬝ p     : by rewrite ap_compose
+             ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (sect f a) ⬝ p       : by rewrite ap_inv
+             ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ sect f a) ⬝ p            : by rewrite ap_con)))
 
     definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ∼ id) :=
     begin
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index 46efce785..9b578bbff 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -312,8 +312,8 @@ namespace sigma
 
   definition comm_equiv_nondep (A B : Type) : (Σ(a : A), B) ≃ Σ(b : B), A :=
   calc
-    (Σ(a : A), B) ≃ A × B : equiv_prod
-              ... ≃ B × A : prod_comm_equiv
+    (Σ(a : A), B) ≃ A × B       : equiv_prod
+              ... ≃ B × A       : prod_comm_equiv
               ... ≃ Σ(b : B), A : equiv_prod
 
   /- ** Universal mapping properties -/
diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean
index 01dbb2e60..38ada9afe 100644
--- a/library/algebra/category/constructions.lean
+++ b/library/algebra/category/constructions.lean
@@ -238,13 +238,15 @@ namespace category
 
   definition postcomposition_functor {x y : D} (h : x ⟶ y)
       : Slice_category D x ⇒ Slice_category D y :=
-  functor.mk (λ a, sigma.mk (to_ob a) (h ∘ ob_hom a))
-             (λ a b f, sigma.mk (hom_hom f)
-       (calc
-         (h ∘ ob_hom b) ∘ hom_hom f = h ∘ (ob_hom b ∘ hom_hom f) : (assoc h (ob_hom b) (hom_hom f))⁻¹
-           ... = h ∘ ob_hom a : congr_arg (λx, h ∘ x) (commute f)))
-             (λ a, rfl)
-             (λ a b c g f, dpair_eq rfl !proof_irrel)
+  functor.mk
+       (λ a, sigma.mk (to_ob a) (h ∘ ob_hom a))
+       (λ a b f,
+         ⟨hom_hom f,
+          calc
+            (h ∘ ob_hom b) ∘ hom_hom f = h ∘ (ob_hom b ∘ hom_hom f) : by rewrite assoc
+                                   ... = h ∘ ob_hom a               : by rewrite commute⟩)
+       (λ a, rfl)
+       (λ a b c g f, dpair_eq rfl !proof_irrel)
 
   -- -- in the following comment I tried to have (A = B) in the type of a == b, but that doesn't solve the problems
   -- definition heq2 {A B : Type} (H : A = B) (a : A) (b : B) := a == b
@@ -347,15 +349,15 @@ namespace category
         (show to_hom c ∘ (hom_src g ∘ hom_src f) = (hom_dst g ∘ hom_dst f) ∘ to_hom a,
          proof
          calc
-         to_hom c ∘ (hom_src g ∘ hom_src f) = (to_hom c ∘ hom_src g) ∘ hom_src f : !assoc
-           ... = (hom_dst g ∘ to_hom b) ∘ hom_src f  : {commute g}
-           ... = hom_dst g ∘ (to_hom b ∘ hom_src f)  : symm !assoc
-           ... = hom_dst g ∘ (hom_dst f ∘ to_hom a)  : {commute f}
-           ... = (hom_dst g ∘ hom_dst f) ∘ to_hom a  : !assoc
+         to_hom c ∘ (hom_src g ∘ hom_src f) = (to_hom c ∘ hom_src g) ∘ hom_src f : by rewrite assoc
+           ... = (hom_dst g ∘ to_hom b) ∘ hom_src f                              : by rewrite commute
+           ... = hom_dst g ∘ (to_hom b ∘ hom_src f)                              : by rewrite assoc
+           ... = hom_dst g ∘ (hom_dst f ∘ to_hom a)                              : by rewrite commute
+           ... = (hom_dst g ∘ hom_dst f) ∘ to_hom a                              : by rewrite assoc
          qed)
        ))
      (λ a, sigma.mk id (sigma.mk id (!id_right ⬝ (symm !id_left))))
-     (λ a b c d h g f, ndtrip_eq       !assoc    !assoc    !proof_irrel)
+     (λ a b c d h g f, ndtrip_eq    !assoc    !assoc    !proof_irrel)
      (λ a b f,         ndtrip_equal !id_left  !id_left  !proof_irrel)
      (λ a b f,         ndtrip_equal !id_right !id_right !proof_irrel)