Define Monoidal categories without depending on category of categories

src/Cat/Categories/Cat.agda

@@ -62,7 +62,7 @@ module _ (ℓ ℓ' : Level) where
 
 -- The following to some extend depends on the category of categories being a
 -- category. In some places it may not actually be needed, however.
-module CatProducts {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
+module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
   private
     :Object: = Object ℂ × Object 𝔻
     :Arrow:  : :Object: → :Object: → Set ℓ'
@@ -153,9 +153,10 @@ module CatProducts {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
 module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
   private
     Catℓ = Cat ℓ ℓ' unprovable
+
   module _ (ℂ 𝔻 : Category ℓ ℓ') where
     private
-      module P = CatProducts ℂ 𝔻
+      module P = CatProduct ℂ 𝔻
 
       instance
         isProduct : IsProduct Catℓ P.proj₁ P.proj₂

src/Cat/Category/Monoid.agda

@@ -12,10 +12,14 @@ module _ (ℓa ℓb : Level) where
   private
     ℓ = lsuc (ℓa ⊔ ℓb)
 
-  -- Might not need this to be able to form products of categories!
-  postulate unprovable : IsCategory (Cat.RawCat ℓa ℓb)
-
-  open HasProducts (Cat.hasProducts unprovable)
+    -- *If* the category of categories existed `_×_` would be equivalent to the
+    -- one brought into scope by doing:
+    --
+    --     open HasProducts (Cat.hasProducts unprovable) using (_×_)
+    --
+    -- Since it doesn't we'll make the following (definitionally equivalent) ad-hoc definition.
+    _×_ : ∀ {ℓa ℓb} → Category ℓa ℓb → Category ℓa ℓb → Category ℓa ℓb
+    ℂ × 𝔻 = Cat.CatProduct.obj ℂ 𝔻
 
   record RawMonoidalCategory : Set ℓ where
     field