From bb379fa19692d524bf043619c6b54577df3fbeec Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 5 Mar 2018 14:50:53 +0100
Subject: [PATCH] Implement category of presheaves

---
 src/Cat/Categories/Fun.agda | 32 +++++++++++++++++++-------------
 1 file changed, 19 insertions(+), 13 deletions(-)

diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 2af9e55..de43087 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -62,9 +62,7 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
     _h⊕g_ = NT[_∘_] {B} {C} {D}
     :isAssociative: : L ≡ R
     :isAssociative: = lemSig (naturalIsProp {F = A} {D})
-      L R (funExt (λ x → isAssociative))
-      where
-        open Category 𝔻
+      L R (funExt (λ x → 𝔻.isAssociative))
 
   private
     module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
@@ -107,14 +105,22 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
   Category.raw Fun = RawFun
 
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-  open import Cat.Categories.Sets
-  open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
+  private
+    open import Cat.Categories.Sets
+    open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
 
-  -- Restrict the functors to Presheafs.
-  RawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
-  RawPresh = record
-    { Object = Presheaf ℂ
-    ; Arrow = NaturalTransformation
-    ; 𝟙 = λ {F} → identity F
-    ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
-    }
+    -- Restrict the functors to Presheafs.
+    rawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
+    rawPresh = record
+      { Object = Presheaf ℂ
+      ; Arrow = NaturalTransformation
+      ; 𝟙 = λ {F} → identity F
+      ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
+      }
+    instance
+      isCategory : IsCategory rawPresh
+      isCategory = Fun.:isCategory: _ _
+
+  Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
+  Category.raw        Presh = rawPresh
+  Category.isCategory Presh = isCategory