From adae95cf68f4e200409ee40e19395cd194d30f81 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Mar 2015 20:13:40 -0700
Subject: [PATCH] refactor(hott/algebra/precategory/functor): remove
 unnecessary annotations

---
 hott/algebra/precategory/functor.hlean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean
index 88d0d4546..249a7109f 100644
--- a/hott/algebra/precategory/functor.hlean
+++ b/hott/algebra/precategory/functor.hlean
@@ -36,8 +36,8 @@ namespace functor
       G (F (ID a)) = G (ID (F a)) : {respect_id F a}
                ... = ID (G (F a)) : respect_id G (F a))
     (λ a b c g f, calc
-      G (F (g ∘ f)) = G (F g ∘ F f)     : respect_comp F g f
-                ... = G (F g) ∘ G (F f) : respect_comp G (F g) (F f))
+      G (F (g ∘ f)) = G (F g ∘ F f)     : by rewrite respect_comp
+                ... = G (F g) ∘ G (F f) : by rewrite respect_comp)
 
   infixr `∘f`:60 := compose