Move functor-stuff to own module

src/Cat/Category.agda

@@ -7,7 +7,6 @@ open import Data.Unit.Base
 open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
 open import Data.Empty
 open import Function
-
 open import Cubical
 
 postulate undefined : {ℓ : Level} → {A : Set ℓ} → A
@@ -31,61 +30,6 @@ record Category {ℓ ℓ'} : Set (lsuc (ℓ' ⊔ ℓ)) where
 
 open Category public
 
-record Functor {ℓc ℓc' ℓd ℓd'} (C : Category {ℓc} {ℓc'}) (D : Category {ℓd} {ℓd'})
-  : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
-  constructor functor
-  private
-    open module C = Category C
-    open module D = Category D
-  field
-    func* : C.Object → D.Object
-    func→ : {dom cod : C.Object} → C.Arrow dom cod → D.Arrow (func* dom) (func* cod)
-    ident   : { c : C.Object } → func→ (C.𝟙 {c}) ≡ D.𝟙 {func* c}
-    -- TODO: Avoid use of ugly explicit arguments somehow.
-    -- This guy managed to do it:
-    --    https://github.com/copumpkin/categories/blob/master/Categories/Functor/Core.agda
-    distrib : { c c' c'' : C.Object} {a : C.Arrow c c'} {a' : C.Arrow c' c''}
-      → func→ (a' C.⊕ a) ≡ func→ a' D.⊕ func→ a
-
-module _ {ℓ ℓ' : Level} {A B C : Category {ℓ} {ℓ'}} (F : Functor B C) (G : Functor A B) where
-  private
-    open module F = Functor F
-    open module G = Functor G
-    open module A = Category A
-    open module B = Category B
-    open module C = Category C
-
-    F* = F.func*
-    F→ = F.func→
-    G* = G.func*
-    G→ = G.func→
-    module _ {a0 a1 a2 : A.Object} {α0 : A.Arrow a0 a1} {α1 : A.Arrow a1 a2} where
-
-      dist : (F→ ∘ G→) (α1 A.⊕ α0) ≡ (F→ ∘ G→) α1 C.⊕ (F→ ∘ G→) α0
-      dist = begin
-        (F→ ∘ G→) (α1 A.⊕ α0)         ≡⟨ refl ⟩
-        F→ (G→ (α1 A.⊕ α0))           ≡⟨ cong F→ G.distrib ⟩
-        F→ ((G→ α1) B.⊕ (G→ α0))      ≡⟨ F.distrib ⟩
-        (F→ ∘ G→) α1 C.⊕ (F→ ∘ G→) α0 ∎
-
-  functor-comp : Functor A C
-  functor-comp =
-    record
-      { func* = F* ∘ G*
-      ; func→ = F→ ∘ G→
-      ; ident = begin
-        (F→ ∘ G→) (A.𝟙) ≡⟨ refl ⟩
-        F→ (G→ (A.𝟙))   ≡⟨ cong F→ G.ident ⟩
-        F→ (B.𝟙)        ≡⟨ F.ident ⟩
-        C.𝟙             ∎
-      ; distrib = dist
-      }
-
--- The identity functor
-identity : {ℓ ℓ' : Level} → {C : Category {ℓ} {ℓ'}} → Functor C C
--- Identity = record { F* = λ x → x ; F→ = λ x → x ; ident = refl ; distrib = refl }
-identity = functor (λ x → x) (λ x → x) (refl) (refl)
-
 module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} { A B : Object ℂ } where
   private
     open module ℂ = Category ℂ

src/Cat/Functor.agda

@@ -0,0 +1,62 @@
+module Cat.Functor where
+
+open import Agda.Primitive
+open import Cubical
+open import Function
+
+open import Cat.Category
+
+record Functor {ℓc ℓc' ℓd ℓd'} (C : Category {ℓc} {ℓc'}) (D : Category {ℓd} {ℓd'})
+  : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
+  constructor functor
+  private
+    open module C = Category C
+    open module D = Category D
+  field
+    func* : C.Object → D.Object
+    func→ : {dom cod : C.Object} → C.Arrow dom cod → D.Arrow (func* dom) (func* cod)
+    ident   : { c : C.Object } → func→ (C.𝟙 {c}) ≡ D.𝟙 {func* c}
+    -- TODO: Avoid use of ugly explicit arguments somehow.
+    -- This guy managed to do it:
+    --    https://github.com/copumpkin/categories/blob/master/Categories/Functor/Core.agda
+    distrib : { c c' c'' : C.Object} {a : C.Arrow c c'} {a' : C.Arrow c' c''}
+      → func→ (a' C.⊕ a) ≡ func→ a' D.⊕ func→ a
+
+module _ {ℓ ℓ' : Level} {A B C : Category {ℓ} {ℓ'}} (F : Functor B C) (G : Functor A B) where
+  private
+    open module F = Functor F
+    open module G = Functor G
+    open module A = Category A
+    open module B = Category B
+    open module C = Category C
+
+    F* = F.func*
+    F→ = F.func→
+    G* = G.func*
+    G→ = G.func→
+    module _ {a0 a1 a2 : A.Object} {α0 : A.Arrow a0 a1} {α1 : A.Arrow a1 a2} where
+
+      dist : (F→ ∘ G→) (α1 A.⊕ α0) ≡ (F→ ∘ G→) α1 C.⊕ (F→ ∘ G→) α0
+      dist = begin
+        (F→ ∘ G→) (α1 A.⊕ α0)         ≡⟨ refl ⟩
+        F→ (G→ (α1 A.⊕ α0))           ≡⟨ cong F→ G.distrib ⟩
+        F→ ((G→ α1) B.⊕ (G→ α0))      ≡⟨ F.distrib ⟩
+        (F→ ∘ G→) α1 C.⊕ (F→ ∘ G→) α0 ∎
+
+  functor-comp : Functor A C
+  functor-comp =
+    record
+      { func* = F* ∘ G*
+      ; func→ = F→ ∘ G→
+      ; ident = begin
+        (F→ ∘ G→) (A.𝟙) ≡⟨ refl ⟩
+        F→ (G→ (A.𝟙))   ≡⟨ cong F→ G.ident ⟩
+        F→ (B.𝟙)        ≡⟨ F.ident ⟩
+        C.𝟙             ∎
+      ; distrib = dist
+      }
+
+-- The identity functor
+identity : {ℓ ℓ' : Level} → {C : Category {ℓ} {ℓ'}} → Functor C C
+-- Identity = record { F* = λ x → x ; F→ = λ x → x ; ident = refl ; distrib = refl }
+identity = functor (λ x → x) (λ x → x) (refl) (refl)