From 0ca11874bcff4ad22de89b06faf406602803fb15 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 24 Feb 2018 12:55:08 +0100
Subject: [PATCH] Remove old name for functor composition

---
 src/Cat/Categories/Cat.agda   | 8 ++++----
 src/Cat/Category/Functor.agda | 3 +--
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 2bb566e..5a0d2dd 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -24,14 +24,14 @@ open Category using (Object ; 𝟙)
 module _ (ℓ ℓ' : Level) where
   private
     module _ {𝔸 𝔹 ℂ 𝔻 : Category ℓ ℓ'} {F : Functor 𝔸 𝔹} {G : Functor 𝔹 ℂ} {H : Functor ℂ 𝔻} where
-      assc : H ∘f (G ∘f F) ≡ (H ∘f G) ∘f F
+      assc : F[ H ∘ F[ G ∘ F ] ] ≡ F[ F[ H ∘ G ] ∘ F ]
       assc = Functor≡ refl refl
 
     module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where
-      ident-r : F ∘f identity ≡ F
+      ident-r : F[ F ∘ identity ] ≡ F
       ident-r = Functor≡ refl refl
 
-      ident-l : identity ∘f F ≡ F
+      ident-l : F[ identity ∘ F ] ≡ F
       ident-l = Functor≡ refl refl
 
   RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
@@ -40,7 +40,7 @@ module _ (ℓ ℓ' : Level) where
       { Object = Category ℓ ℓ'
       ; Arrow = Functor
       ; 𝟙 = identity
-      ; _∘_ = _∘f_
+      ; _∘_ = F[_∘_]
       }
   private
     open RawCategory RawCat
diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index 7a2e565..d648728 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -124,9 +124,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
         ; isDistributive = dist
         }
 
-  F[_∘_] _∘f_ : Functor A C
+  F[_∘_] : Functor A C
   raw F[_∘_] = _∘fr_
-  _∘f_ = F[_∘_]
 
 -- The identity functor
 identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C