From 9e96e704e8fabbcad852b7a47836ba8716bc8b0f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 21 Feb 2018 13:40:24 +0100
Subject: [PATCH] Update `Fun` according to new naming policy

---
 src/Cat/Categories/Fun.agda      | 12 ++++++------
 src/Cat/Category/Properties.agda |  1 -
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index ada60d2..ba492d0 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -21,7 +21,7 @@ open import Cat.Equality
 open Equality.Data.Product
 
 module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
-  open Category hiding ( _∘_ ; Arrow )
+  open Category using (Object ; 𝟙)
   open Functor
 
   module _ (F G : Functor ℂ 𝔻) where
@@ -70,7 +70,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     where
       module F = Functor F
       F→ = F.func→
-      module 𝔻 = IsCategory (isCategory 𝔻)
+      module 𝔻 = Category 𝔻
 
   identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F
   identityNat F = identityTrans F , identityNatural F
@@ -95,13 +95,13 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
       𝔻 [ H.func→ f ∘ (θ ∘nt η) A ]     ∎
       where
-        open IsCategory (isCategory 𝔻)
+        open Category 𝔻
 
     NatComp = _:⊕:_
 
   private
     module _ {F G : Functor ℂ 𝔻} where
-      module 𝔻 = IsCategory (isCategory 𝔻)
+      module 𝔻 = Category 𝔻
 
       transformationIsSet : isSet (Transformation F G)
       transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C)   (λ l → q l C) i j
@@ -139,7 +139,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       :assoc: = lemSig (naturalIsProp {F = A} {D})
         L R (funExt (λ x → assoc))
         where
-          open IsCategory (isCategory 𝔻)
+          open Category 𝔻
 
     module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
       private
@@ -181,7 +181,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
       }
 
   Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
-  raw Fun = RawFun
+  Category.raw Fun = RawFun
 
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   open import Cat.Categories.Sets
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index a656b4c..b001344 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -14,7 +14,6 @@ open Equality.Data.Product
 
 module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.Arrow ℂ A B) where
   open Category ℂ
-  open IsCategory (isCategory)
 
   iso-is-epi : Isomorphism f → Epimorphism {X = X} f
   iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin