diff --git a/Cubical/Papers/SmashProducts.agda b/Cubical/Papers/SmashProducts.agda
index 25aa062464..3b6f12bccc 100644
--- a/Cubical/Papers/SmashProducts.agda
+++ b/Cubical/Papers/SmashProducts.agda
@@ -41,10 +41,10 @@ open WCat2 using (PointedCat)
 open WCat3 using (isMonoidalWildCat)
 
 -- Definition 4 (Symmetric Monoidal wild categories)
-open WCat3 using (SymmetricMonoidalPrecat)
+open WCat3 using (isSymmetricWildCat)
 
 --- 2.2 Smash Products
--- Definition 5 (Smash products -- note: defined as a coproduct in the
+-- Definition 5 (Smash products -- note: defined as a pushout in the
 -- library. E.g. the ⟨ x , y ⟩ constructor here is simply
 -- inr(x,y). Also note that pushₗ and pushᵣ are inverted with this
 -- definition.)
diff --git a/Cubical/WildCat/BraidedSymmetricMonoidal.agda b/Cubical/WildCat/BraidedSymmetricMonoidal.agda
index 7f0287332d..e6042c4625 100644
--- a/Cubical/WildCat/BraidedSymmetricMonoidal.agda
+++ b/Cubical/WildCat/BraidedSymmetricMonoidal.agda
@@ -104,6 +104,6 @@ module _ (M : WildCat ℓ ℓ') where
       hexagon : HexagonType₁ isMonoidal Braid
       symBraiding : isSymmetricBraiding isMonoidal Braid
 
-SymmetricMonoidalPrecat : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ'))
-SymmetricMonoidalPrecat ℓ ℓ' =
+SymmetricMonoidalWildCat : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ'))
+SymmetricMonoidalWildCat ℓ ℓ' =
   Σ[ C ∈ WildCat ℓ ℓ' ] isSymmetricWildCat C