diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 3ae0c4b..95c0e15 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -151,7 +151,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
     private
       module P = CatProduct ℂ 𝔻
 
-      rawProduct : RawProduct {ℂ = Catℓ} ℂ 𝔻
+      rawProduct : RawProduct Catℓ ℂ 𝔻
       RawProduct.obj   rawProduct = P.obj
       RawProduct.proj₁ rawProduct = P.proj₁
       RawProduct.proj₂ rawProduct = P.proj₂
@@ -159,7 +159,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
       isProduct : IsProduct Catℓ rawProduct
       IsProduct.isProduct isProduct = P.isProduct
 
-    product : Product {ℂ = Catℓ} ℂ 𝔻
+    product : Product Catℓ ℂ 𝔻
     Product.raw       product = rawProduct
     Product.isProduct product = isProduct
 
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 970ae96..adcbfc3 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -64,15 +64,17 @@ module _ {ℓ : Level} where
             lem : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g
             proj₁ lem = refl
             proj₂ lem = refl
-        rawProduct : RawProduct {ℂ = 𝓢} 0A 0B
+
+        rawProduct : RawProduct 𝓢 0A 0B
         RawProduct.obj   rawProduct = 0A×0B
         RawProduct.proj₁ rawProduct = Data.Product.proj₁
         RawProduct.proj₂ rawProduct = Data.Product.proj₂
+
         isProduct : IsProduct 𝓢 rawProduct
         IsProduct.isProduct isProduct {X = X} f g
           = (f &&& g) , lem {0X = X} f g
 
-      product : Product {ℂ = 𝓢} 0A 0B
+      product : Product 𝓢 0A 0B
       Product.raw       product = rawProduct
       Product.isProduct product = isProduct
 
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 80baaab..c68afd7 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -9,14 +9,14 @@ open import Cat.Category hiding (module Propositionality)
 open Category
 
 module _ {ℓa ℓb : Level} where
-  record RawProduct {ℂ : Category ℓa ℓb} (A B : Object ℂ) : Set (ℓa ⊔ ℓb) where
+  record RawProduct (ℂ : Category ℓa ℓb) (A B : Object ℂ) : Set (ℓa ⊔ ℓb) where
     no-eta-equality
     field
       obj : Object ℂ
       proj₁ : ℂ [ obj , A ]
       proj₂ : ℂ [ obj , B ]
 
-  record IsProduct (ℂ : Category ℓa ℓb) {A B : Object ℂ} (raw : RawProduct {ℂ = ℂ} A B) : Set (ℓa ⊔ ℓb) where
+  record IsProduct (ℂ : Category ℓa ℓb) {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 ])
@@ -27,16 +27,16 @@ module _ {ℓa ℓb : Level} where
       → ℂ [ X , obj ]
     _P[_×_] π₁ π₂ = P.proj₁ (isProduct π₁ π₂)
 
-  record Product {ℂ : Category ℓa ℓb} (A B : Object ℂ) : Set (ℓa ⊔ ℓb) where
+  record Product (ℂ : Category ℓa ℓb) (A B : Object ℂ) : Set (ℓa ⊔ ℓb) where
     field
-      raw        : RawProduct {ℂ = ℂ} A B
+      raw        : RawProduct ℂ A B
       isProduct  : IsProduct ℂ {A} {B} raw
 
     open IsProduct isProduct public
 
   record HasProducts (ℂ : Category ℓa ℓb) : Set (ℓa ⊔ ℓb) where
     field
-      product : ∀ (A B : Object ℂ) → Product {ℂ = ℂ} A B
+      product : ∀ (A B : Object ℂ) → Product ℂ A B
 
     module _ (A B : Object ℂ) where
       open Product (product A B)