diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean
index 5f05943b4..2fd0ca8ed 100644
--- a/hott/algebra/category/functor.hlean
+++ b/hott/algebra/category/functor.hlean
@@ -30,12 +30,12 @@ namespace functor
   functor.mk
     (λ x, G (F x))
     (λ a b f, G (F f))
-    (λ a, calc
+    (λ a, abstract calc
       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
+               ... = ID (G (F a)) : by rewrite respect_id end)
+    (λ a b c g f, abstract calc
       G (F (g ∘ f)) = G (F g ∘ F f)     : by rewrite respect_comp
-                ... = G (F g) ∘ G (F f) : by rewrite respect_comp)
+                ... = G (F g) ∘ G (F f) : by rewrite respect_comp end)
 
   infixr `∘f`:60 := functor.compose
 
diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean
index 0b9ac5221..7098113c7 100644
--- a/hott/algebra/category/nat_trans.hlean
+++ b/hott/algebra/category/nat_trans.hlean
@@ -21,12 +21,13 @@ namespace nat_trans
   nat_trans.mk
     (λ a, η a ∘ θ a)
     (λ a b f,
-      calc
+      abstract calc
         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)
+                      ... = (η b ∘ θ b) ∘ F f : by rewrite assoc
+      end)
 
   infixr `∘n`:60 := nat_trans.compose