From 8362498b564839da4d69aa11520db3e7b10aad98 Mon Sep 17 00:00:00 2001
From: favonia <favonia@gmail.com>
Date: Thu, 8 Jun 2017 17:48:26 -0600
Subject: [PATCH] Remove AddGroup symbol.

---
 algebra/direct_sum.hlean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean
index e4fdeef..e691287 100644
--- a/algebra/direct_sum.hlean
+++ b/algebra/direct_sum.hlean
@@ -124,7 +124,7 @@ namespace group
   dirsum_elim (λi, dirsum_incl Y' i ∘g f i)
 
   theorem dirsum_functor_compose (f' : Πi, Y' i →g Y'' i) (f : Πi, Y i →g Y' i) :
-    dirsum_functor f' ∘a dirsum_functor f ~ dirsum_functor (λi, f' i ∘a f i) :=
+    dirsum_functor f' ∘g dirsum_functor f ~ dirsum_functor (λi, f' i ∘g f i) :=
   begin
     apply dirsum_homotopy,
     intro i y, reflexivity,