From a4890a42cf8458b34e53eab49ccb94fc01709ce3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 5 Mar 2018 11:13:37 +0100
Subject: [PATCH] Define Monoidal categories without depending on category of
 categories

---
 src/Cat/Categories/Cat.agda  |  5 +++--
 src/Cat/Category/Monoid.agda | 12 ++++++++----
 2 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 146fd96..c7f1026 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/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₂
diff --git a/src/Cat/Category/Monoid.agda b/src/Cat/Category/Monoid.agda
index 3323487..6cce193 100644
--- a/src/Cat/Category/Monoid.agda
+++ b/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