From e3d2c0d39ee5d6baec9a5ec00a85042ecb0a1bc8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 8 Jan 2018 22:29:29 +0100
Subject: [PATCH] Move category of Categories to own module

---
 src/Category.agda                | 45 --------------------------
 src/Category/Categories/Cat.agda | 55 ++++++++++++++++++++++++++++++++
 2 files changed, 55 insertions(+), 45 deletions(-)
 create mode 100644 src/Category/Categories/Cat.agda

diff --git a/src/Category.agda b/src/Category.agda
index b1f7c88..568f93b 100644
--- a/src/Category.agda
+++ b/src/Category.agda
@@ -184,51 +184,6 @@ Opposite ℂ =
   where
     open module ℂ = Category ℂ
 
--- The category of categories
-module _ {ℓ ℓ' : Level} where
-  private
-    _⊛_ = functor-comp
-    module _ {A B C D : Category {ℓ} {ℓ'}} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
-      assc : h ⊛ (g ⊛ f) ≡ (h ⊛ g) ⊛ f
-      assc = {!!}
-
-    module _ {A B : Category {ℓ} {ℓ'}} where
-      lift-eq : (f g : Functor A B)
-        → (eq* : Functor.func* f ≡ Functor.func* g)
-        -- TODO: Must transport here using the equality from above.
-        -- Reason:
-        --   func→  : Arrow A dom cod → Arrow B (func* dom) (func* cod)
-        --   func→₁ : Arrow A dom cod → Arrow B (func*₁ dom) (func*₁ cod)
-        -- In other words, func→ and func→₁ does not have the same type.
-  --      → Functor.func→ f ≡ Functor.func→ g
-  --      → Functor.ident f ≡ Functor.ident g
-  --       → Functor.distrib f ≡ Functor.distrib g
-        → f ≡ g
-      lift-eq
-        (functor func* func→ idnt distrib)
-        (functor func*₁ func→₁ idnt₁ distrib₁)
-        eq-func* = {!!}
-
-    module _ {A B : Category {ℓ} {ℓ'}} {f : Functor A B} where
-      idHere = identity {ℓ} {ℓ'} {A}
-      lem : (Functor.func* f) ∘ (Functor.func* idHere) ≡ Functor.func* f
-      lem = refl
-      ident-r : f ⊛ identity ≡ f
-      ident-r = lift-eq (f ⊛ identity) f refl
-      ident-l : identity ⊛ f ≡ f
-      ident-l = {!!}
-
-  CatCat : Category {lsuc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'}
-  CatCat =
-    record
-      { Object = Category {ℓ} {ℓ'}
-      ; Arrow = Functor
-      ; 𝟙 = identity
-      ; _⊕_ = functor-comp
-      ; assoc = {!!}
-      ; ident = ident-r , ident-l
-      }
-
 Hom : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → (A B : Object ℂ) → Set ℓ'
 Hom {ℂ = ℂ} A B = Arrow ℂ A B
 
diff --git a/src/Category/Categories/Cat.agda b/src/Category/Categories/Cat.agda
new file mode 100644
index 0000000..79efc49
--- /dev/null
+++ b/src/Category/Categories/Cat.agda
@@ -0,0 +1,55 @@
+{-# OPTIONS --cubical #-}
+
+module Category.Categories.Cat where
+
+open import Agda.Primitive
+open import Cubical
+open import Function
+open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
+
+open import Category
+
+-- The category of categories
+module _ {ℓ ℓ' : Level} where
+  private
+    _⊛_ = functor-comp
+    module _ {A B C D : Category {ℓ} {ℓ'}} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
+      assc : h ⊛ (g ⊛ f) ≡ (h ⊛ g) ⊛ f
+      assc = {!!}
+
+    module _ {A B : Category {ℓ} {ℓ'}} where
+      lift-eq : (f g : Functor A B)
+        → (eq* : Functor.func* f ≡ Functor.func* g)
+        -- TODO: Must transport here using the equality from above.
+        -- Reason:
+        --   func→  : Arrow A dom cod → Arrow B (func* dom) (func* cod)
+        --   func→₁ : Arrow A dom cod → Arrow B (func*₁ dom) (func*₁ cod)
+        -- In other words, func→ and func→₁ does not have the same type.
+  --      → Functor.func→ f ≡ Functor.func→ g
+  --      → Functor.ident f ≡ Functor.ident g
+  --       → Functor.distrib f ≡ Functor.distrib g
+        → f ≡ g
+      lift-eq
+        (functor func* func→ idnt distrib)
+        (functor func*₁ func→₁ idnt₁ distrib₁)
+        eq-func* = {!!}
+
+    module _ {A B : Category {ℓ} {ℓ'}} {f : Functor A B} where
+      idHere = identity {ℓ} {ℓ'} {A}
+      lem : (Functor.func* f) ∘ (Functor.func* idHere) ≡ Functor.func* f
+      lem = refl
+      ident-r : f ⊛ identity ≡ f
+      ident-r = lift-eq (f ⊛ identity) f refl
+      ident-l : identity ⊛ f ≡ f
+      ident-l = {!!}
+
+  CatCat : Category {lsuc (ℓ ⊔ ℓ')} {ℓ ⊔ ℓ'}
+  CatCat =
+    record
+      { Object = Category {ℓ} {ℓ'}
+      ; Arrow = Functor
+      ; 𝟙 = identity
+      ; _⊕_ = functor-comp
+      ; assoc = {!!}
+      ; ident = ident-r , ident-l
+      }