still allow definitional commutativity with projecting to the carrier

Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Base.agda

@@ -92,20 +92,24 @@ module Construction (R : CommRing ℓ) where
                                     ⋆-assoc ⋆-rdist-+ ⋆-ldist-+ ·-lid ⋆-assoc-·
 
 
-opaque
-  _[_] : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R (ℓ-max ℓ ℓ')
-  fst (R [ I ]) = Construction.R[_] R I
-  snd (R [ I ]) = makeCommAlgebraStr _ _ _ _ _ _ _ isCommAlgebra
-    where open Construction R
 
-opaque
-  unfolding _[_]
+module _ (R : CommRing ℓ) (I : Type ℓ') where
+  open Construction R
+  opaque
+    freeCAlgStr : CommAlgebraStr R (R[ I ])
+    freeCAlgStr = makeCommAlgebraStr _ _ _ _ _ _ _ isCommAlgebra
+
+_[_] : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R (ℓ-max ℓ ℓ')
+fst (R [ I ]) = Construction.R[_] R I
+snd (R [ I ]) = freeCAlgStr R I
 
+_[_]ᵣ : (R : CommRing ℓ) (I : Type ℓ') → CommRing (ℓ-max ℓ ℓ')
+(R [ I ]ᵣ) = CommAlgebra→CommRing (R [ I ])
+
+opaque
   const : {R : CommRing ℓ} {I : Type ℓ'} → ⟨ R ⟩ → ⟨ R [ I ] ⟩
   const = Construction.const
 
 opaque
-  unfolding _[_]
-
   var : {R : CommRing ℓ} {I : Type ℓ'} → I → ⟨ R [ I ] ⟩
   var = Construction.var

Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda

@@ -70,7 +70,7 @@ module Theory {R : CommRing ℓ} {I : Type ℓ'} where
 
     private
       opaque
-        unfolding const
+        unfolding const freeCAlgStr
 
         on- : {x : ⟨ R [ I ] ⟩} → P x → P (- x)
         on- {x} Px = subst P (minusByMult x) (on· onConst Px)
@@ -86,7 +86,7 @@ module Theory {R : CommRing ℓ} {I : Type ℓ'} where
       mkPathP _ = isProp→PathP λ i → isPropP
 
     opaque
-      unfolding _[_] var const
+      unfolding var const freeCAlgStr
 
       elimProp : ((x : _) → P x)
 
@@ -175,7 +175,7 @@ module Theory {R : CommRing ℓ} {I : Type ℓ'} where
 --    imageOf1Works = ⋆IdL 1a
 
     opaque
-      unfolding _[_] const
+      unfolding const
 
       inducedMap : ⟨ R [ I ] ⟩ → ⟨ A ⟩
       inducedMap (C.var x) = φ x
@@ -224,7 +224,7 @@ module Theory {R : CommRing ℓ} {I : Type ℓ'} where
       open IsAlgebraHom
 
       opaque
-        unfolding inducedMap
+        unfolding inducedMap freeCAlgStr
 
         inducedHom : CommAlgebraHom (R [ I ]) A
         inducedHom .fst = inducedMap