diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean
index 249a7109f8..0a0d867034 100644
--- a/hott/algebra/precategory/functor.hlean
+++ b/hott/algebra/precategory/functor.hlean
@@ -33,8 +33,8 @@ namespace functor
     (λ x, G (F x))
     (λ a b f, G (F f))
     (λ a, calc
-      G (F (ID a)) = G (ID (F a)) : {respect_id F a}
-               ... = ID (G (F a)) : respect_id G (F a))
+      G (F (ID a)) = G (ID (F a)) : by rewrite respect_id
+               ... = ID (G (F a)) : by rewrite respect_id)
     (λ a b c g f, calc
       G (F (g ∘ f)) = G (F g ∘ F f)     : by rewrite respect_comp
                 ... = G (F g) ∘ G (F f) : by rewrite respect_comp)
diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean
index 164aaba983..fb9fde881f 100644
--- a/hott/algebra/precategory/iso.hlean
+++ b/hott/algebra/precategory/iso.hlean
@@ -202,7 +202,7 @@ namespace iso
     (λ c g h H,
       calc
         g = id ∘ g                    : by rewrite id_left
-      ... = (retraction_of f ∘ f) ∘ g : by rewrite -retraction_comp
+      ... = (retraction_of f ∘ f) ∘ g : by rewrite retraction_comp
       ... = (retraction_of f ∘ f) ∘ h : by rewrite [-assoc, H, -assoc]
       ... = id ∘ h                    : by rewrite retraction_comp
       ... = h                         : by rewrite id_left)