From 2e630d08db08eb56baf0679717dc0cc8f2762202 Mon Sep 17 00:00:00 2001
From: Jordan Mitchell Barrett <90195985+barrettj12@users.noreply.github.com>
Date: Wed, 15 Dec 2021 16:22:37 +0100
Subject: [PATCH] Category of categories (#642)

* Add CAT

* Make `Cat` a precategory

* Name change
---
 Cubical/Categories/Instances/Categories.agda | 25 ++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 Cubical/Categories/Instances/Categories.agda

diff --git a/Cubical/Categories/Instances/Categories.agda b/Cubical/Categories/Instances/Categories.agda
new file mode 100644
index 0000000000..7ce6b89a2f
--- /dev/null
+++ b/Cubical/Categories/Instances/Categories.agda
@@ -0,0 +1,25 @@
+-- The (pre)category of (small) categories
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Instances.Categories where
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Category.Precategory
+open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.Functor.Properties
+open import Cubical.Foundations.Prelude
+
+
+module _ (ℓ ℓ' : Level) where
+  open Precategory
+
+  CatPrecategory : Precategory (ℓ-suc (ℓ-max ℓ ℓ')) (ℓ-max ℓ ℓ')
+  CatPrecategory .ob = Category ℓ ℓ'
+  CatPrecategory .Hom[_,_] = Functor
+  CatPrecategory .id = 𝟙⟨ _ ⟩
+  CatPrecategory ._⋆_ G H = H ∘F G
+  CatPrecategory .⋆IdL _ = F-lUnit
+  CatPrecategory .⋆IdR _ = F-rUnit
+  CatPrecategory .⋆Assoc _ _ _ = F-assoc
+
+-- TODO: what is required for Functor C D to be a set?