Factor out objects

src/Cat/Categories/Cat.agda

@@ -156,7 +156,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
       RawProduct.proj₁ rawProduct = P.proj₁
       RawProduct.proj₂ rawProduct = P.proj₂
 
-      isProduct : IsProduct Catℓ rawProduct
+      isProduct : IsProduct Catℓ _ _ rawProduct
       IsProduct.isProduct isProduct = P.isProduct
 
     product : Product Catℓ ℂ 𝔻

src/Cat/Categories/Sets.agda

@@ -70,7 +70,7 @@ module _ {ℓ : Level} where
         RawProduct.proj₁ rawProduct = Data.Product.proj₁
         RawProduct.proj₂ rawProduct = Data.Product.proj₂
 
-        isProduct : IsProduct 𝓢 rawProduct
+        isProduct : IsProduct 𝓢 _ _ rawProduct
         IsProduct.isProduct isProduct {X = X} f g
           = (f &&& g) , lem {0X = X} f g
 

src/Cat/Category/Product.agda

@@ -10,30 +10,31 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 
   open Category ℂ
 
-  record RawProduct (A B : Object) : Set (ℓa ⊔ ℓb) where
-    no-eta-equality
-    field
-      obj : Object
-      proj₁ : ℂ [ obj , A ]
-      proj₂ : ℂ [ obj , B ]
+  module _ (A B : Object) where
+    record RawProduct : Set (ℓa ⊔ ℓb) where
+      no-eta-equality
+      field
+        obj : Object
+        proj₁ : ℂ [ obj , A ]
+        proj₂ : ℂ [ obj , B ]
 
-  record IsProduct {A B : Object} (raw : RawProduct A B) : Set (ℓa ⊔ ℓb) where
-    open RawProduct raw public
-    field
-      isProduct : ∀ {X : Object} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
-        → ∃![ x ] (ℂ [ proj₁ ∘ x ] ≡ x₁ P.× ℂ [ proj₂ ∘ x ] ≡ x₂)
+    record IsProduct (raw : RawProduct) : Set (ℓa ⊔ ℓb) where
+      open RawProduct raw public
+      field
+        isProduct : ∀ {X : Object} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
+          → ∃![ x ] (ℂ [ proj₁ ∘ x ] ≡ x₁ P.× ℂ [ proj₂ ∘ x ] ≡ x₂)
 
-    -- | Arrow product
-    _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
-      → ℂ [ X , obj ]
-    _P[_×_] π₁ π₂ = P.proj₁ (isProduct π₁ π₂)
+      -- | Arrow product
+      _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ])
+        → ℂ [ X , obj ]
+      _P[_×_] π₁ π₂ = P.proj₁ (isProduct π₁ π₂)
 
-  record Product (A B : Object) : Set (ℓa ⊔ ℓb) where
-    field
-      raw        : RawProduct A B
-      isProduct  : IsProduct {A} {B} raw
+    record Product : Set (ℓa ⊔ ℓb) where
+      field
+        raw        : RawProduct
+        isProduct  : IsProduct raw
 
-    open IsProduct isProduct public
+      open IsProduct isProduct public
 
   record HasProducts : Set (ℓa ⊔ ℓb) where
     field