Category of categories (#642)

* Add CAT * Make `Cat` a precategory * Name change
agda · Dec 15, 2021 · 2e630d0 · 2e630d0
1 parent e206558
commit 2e630d0
Showing 1 changed file with 25 additions and 0 deletions.
diff --git a/Cubical/Categories/Instances/Categories.agda 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?