diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 757c5cc..4fb6237 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -87,18 +87,18 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object 
     q = lemPropF propIsProduct p
 
 module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
-  (let module ℂ = Category ℂ) {A B : ℂ.Object} where
+  (let module ℂ = Category ℂ) {𝓐 𝓑 : ℂ.Object} where
 
   open P
 
   module _ where
     raw : RawCategory _ _
     raw = record
-      { Object = Σ[ X ∈ ℂ.Object ] ℂ.Arrow X A × ℂ.Arrow X B
-      ; Arrow = λ{ (X , x0 , x1) (Y , y0 , y1)
-        → Σ[ f ∈ ℂ.Arrow X Y ]
-            ℂ [ y0 ∘ f ] ≡ x0
-          × ℂ [ y1 ∘ f ] ≡ x1
+      { Object = Σ[ X ∈ ℂ.Object ] ℂ.Arrow X 𝓐 × ℂ.Arrow X 𝓑
+      ; Arrow = λ{ (A , a0 , a1) (B , b0 , b1)
+        → Σ[ f ∈ ℂ.Arrow A B ]
+            ℂ [ b0 ∘ f ] ≡ a0
+          × ℂ [ b1 ∘ f ] ≡ a1
           }
       ; identity = λ{ {X , f , g} → ℂ.identity {X} , ℂ.rightIdentity , ℂ.rightIdentity}
       ; _<<<_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1} (f , f0 , f1) (g , g0 , g1)
@@ -176,7 +176,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≅_)
       step0
         : ((X , xa , xb) ≡ (Y , ya , yb))
-        ≅ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
+        ≅ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝓐) xa ya) × (PathP (λ i → ℂ.Arrow (p i) 𝓑) xb yb))
       step0
         = (λ p → cong fst p , cong-d (fst ∘ snd) p , cong-d (snd ∘ snd) p)
         -- , (λ x  → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
@@ -203,12 +203,12 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
            p
 
       step1
-        : (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
+        : (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝓐) xa ya) × (PathP (λ i → ℂ.Arrow (p i) 𝓑) xb yb))
         ≅ Σ (X ℂ.≊ Y) (λ iso
           → let p = ℂ.isoToId iso
           in
-          ( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
-          × PathP (λ i → ℂ.Arrow (p i) B) xb yb
+          ( PathP (λ i → ℂ.Arrow (p i) 𝓐) xa ya)
+          × PathP (λ i → ℂ.Arrow (p i) 𝓑) xb yb
           )
       step1
         = symIso
@@ -216,7 +216,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
               {A = (X ℂ.≊ Y)}
               {B = (X ≡ Y)}
               (ℂ.groupoidObject _ _)
-              {Q = \ p → (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)}
+              {Q = \ p → (PathP (λ i → ℂ.Arrow (p i) 𝓐) xa ya) × (PathP (λ i → ℂ.Arrow (p i) 𝓑) xb yb)}
               ℂ.isoToId
               (symIso (_ , ℂ.asTypeIso {X} {Y}) .snd)
             )
@@ -225,8 +225,8 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
         : Σ (X ℂ.≊ Y) (λ iso
           → let p = ℂ.isoToId iso
           in
-          ( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
-          × PathP (λ i → ℂ.Arrow (p i) B) xb yb
+          ( PathP (λ i → ℂ.Arrow (p i) 𝓐) xa ya)
+          × PathP (λ i → ℂ.Arrow (p i) 𝓑) xb yb
           )
         ≅ ((X , xa , xb) ≊ (Y , ya , yb))
       step2
@@ -243,10 +243,10 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
             iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~
             p : X ≡ Y
             p = ℂ.isoToId iso
-            pA : ℂ.Arrow X A ≡ ℂ.Arrow Y A
-            pA = cong (λ x → ℂ.Arrow x A) p
-            pB : ℂ.Arrow X B ≡ ℂ.Arrow Y B
-            pB = cong (λ x → ℂ.Arrow x B) p
+            pA : ℂ.Arrow X 𝓐 ≡ ℂ.Arrow Y 𝓐
+            pA = cong (λ x → ℂ.Arrow x 𝓐) p
+            pB : ℂ.Arrow X 𝓑 ≡ ℂ.Arrow Y 𝓑
+            pB = cong (λ x → ℂ.Arrow x 𝓑) p
             k0 = begin
               coe pB xb ≡⟨ ℂ.coe-dom iso ⟩
               xb ℂ.<<< fst f~ ≡⟨ snd (snd f~) ⟩
@@ -264,10 +264,10 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
             (Σ≡ refl (ℂ.propIsomorphism _ _ _)))
         , funExt (λ{ (f , _) → lemSig propIsomorphism _ _ (Σ≡ refl (propEqs _ _ _))})
           where
-          prop0 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) A) xa ya)
-          prop0 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) A) xa x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) ya
-          prop1 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) B) xb yb)
-          prop1 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) B) xb x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) yb
+          prop0 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) 𝓐) xa ya)
+          prop0 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) 𝓐) xa x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) ya
+          prop1 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) 𝓑) xb yb)
+          prop1 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) 𝓑) xb x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) yb
       -- One thing to watch out for here is that the isomorphisms going forwards
       -- must compose to give idToIso
       iso
@@ -297,34 +297,34 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
 
   open Category cat
 
-  lemma : Terminal ≃ Product ℂ A B
-  lemma = fromIsomorphism Terminal (Product ℂ A B) (f , g , inv)
+  lemma : Terminal ≃ Product ℂ 𝓐 𝓑
+  lemma = fromIsomorphism Terminal (Product ℂ 𝓐 𝓑) (f , g , inv)
     where
-    f : Terminal → Product ℂ A B
+    f : Terminal → Product ℂ 𝓐 𝓑
     f ((X , x0 , x1) , uniq) = p
       where
-      rawP : RawProduct ℂ A B
+      rawP : RawProduct ℂ 𝓐 𝓑
       rawP = record
         { object = X
         ; fst = x0
         ; snd = x1
         }
       -- open RawProduct rawP renaming (fst to x0 ; snd to x1)
-      module _ {Y : ℂ.Object} (p0 : ℂ [ Y , A ]) (p1 : ℂ [ Y , B ]) where
+      module _ {Y : ℂ.Object} (p0 : ℂ [ Y , 𝓐 ]) (p1 : ℂ [ Y , 𝓑 ]) where
         uy : isContr (Arrow (Y , p0 , p1) (X , x0 , x1))
         uy = uniq {Y , p0 , p1}
         open Σ uy renaming (fst to Y→X ; snd to contractible)
         open Σ Y→X renaming (fst to p0×p1 ; snd to cond)
         ump : ∃![ f×g ] (ℂ [ x0 ∘ f×g ] ≡ p0 P.× ℂ [ x1 ∘ f×g ] ≡ p1)
         ump = p0×p1 , cond , λ {y} x → let k = contractible (y , x) in λ i → fst (k i)
-      isP : IsProduct ℂ A B rawP
+      isP : IsProduct ℂ 𝓐 𝓑 rawP
       isP = record { ump = ump }
-      p : Product ℂ A B
+      p : Product ℂ 𝓐 𝓑
       p = record
         { raw = rawP
         ; isProduct = isP
         }
-    g : Product ℂ A B → Terminal
+    g : Product ℂ 𝓐 𝓑 → Terminal
     g p = o , t
       where
       module p = Product p
@@ -375,7 +375,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
     inv : AreInverses f g
     inv = funExt ve-re , funExt re-ve
 
-  propProduct : isProp (Product ℂ A B)
+  propProduct : isProp (Product ℂ 𝓐 𝓑)
   propProduct = equivPreservesNType {n = ⟨-1⟩} lemma Propositionality.propTerminal
 
 module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where