diff --git a/Cubical/Algebra/Algebra/Base.agda b/Cubical/Algebra/Algebra/Base.agda
index 97afcced0f..a49583a279 100644
--- a/Cubical/Algebra/Algebra/Base.agda
+++ b/Cubical/Algebra/Algebra/Base.agda
@@ -50,7 +50,7 @@ record IsAlgebra (R : Ring ℓ) {A : Type ℓ'}
 
   open IsLeftModule +IsLeftModule public
 
-  isRing : IsRing _ _ _ _ _
+  isRing : IsRing 0a 1a _+_ _·_ (-_)
   isRing = isring (IsLeftModule.+IsAbGroup +IsLeftModule) ·IsMonoid ·DistR+ ·DistL+
   open IsRing isRing public
     hiding (_-_; +Assoc; +IdL; +InvL; +IdR; +InvR; +Comm; ·DistR+; ·DistL+; is-set)
diff --git a/Cubical/Algebra/CommAlgebra/Base.agda b/Cubical/Algebra/CommAlgebra/Base.agda
index 4022db273f..f46ac4b814 100644
--- a/Cubical/Algebra/CommAlgebra/Base.agda
+++ b/Cubical/Algebra/CommAlgebra/Base.agda
@@ -29,8 +29,7 @@ record IsCommAlgebra (R : CommRing ℓ) {A : Type ℓ'}
                      (0a : A) (1a : A)
                      (_+_ : A → A → A) (_·_ : A → A → A) (-_ : A → A)
                      (_⋆_ : ⟨ R ⟩ → A → A) : Type (ℓ-max ℓ ℓ') where
-
-  constructor iscommalgebra
+  no-eta-equality
 
   field
     isAlgebra : IsAlgebra (CommRing→Ring R) 0a 1a _+_ _·_ -_ _⋆_
@@ -41,8 +40,7 @@ record IsCommAlgebra (R : CommRing ℓ) {A : Type ℓ'}
 unquoteDecl IsCommAlgebraIsoΣ = declareRecordIsoΣ IsCommAlgebraIsoΣ (quote IsCommAlgebra)
 
 record CommAlgebraStr (R : CommRing ℓ) (A : Type ℓ') : Type (ℓ-max ℓ ℓ') where
-
-  constructor commalgebrastr
+  no-eta-equality
 
   field
     0a             : A
@@ -60,6 +58,8 @@ record CommAlgebraStr (R : CommRing ℓ) (A : Type ℓ') : Type (ℓ-max ℓ ℓ
   infixl 7 _⋆_
   infixl 6 _+_
 
+unquoteDecl CommAlgebraStrIsoΣ = declareRecordIsoΣ CommAlgebraStrIsoΣ (quote CommAlgebraStr)
+
 CommAlgebra : (R : CommRing ℓ) → ∀ ℓ' → Type (ℓ-max ℓ (ℓ-suc ℓ'))
 CommAlgebra R ℓ' = Σ[ A ∈ Type ℓ' ] CommAlgebraStr R A
 
@@ -67,15 +67,34 @@ module _ {R : CommRing ℓ} where
   open CommRingStr (snd R) using (1r) renaming (_+_ to _+r_; _·_ to _·s_)
 
   CommAlgebraStr→AlgebraStr : {A : Type ℓ'} → CommAlgebraStr R A → AlgebraStr (CommRing→Ring R) A
-  CommAlgebraStr→AlgebraStr (commalgebrastr _ _ _ _ _ _ (iscommalgebra isAlgebra ·-comm)) =
-    algebrastr _ _ _ _ _ _ isAlgebra
+  CommAlgebraStr→AlgebraStr {A = A} cstr = x
+    where open AlgebraStr
+          x : AlgebraStr (CommRing→Ring R) A
+          0a x = _
+          1a x = _
+          _+_ x = _
+          _·_ x = _
+          - x = _
+          _⋆_ x = _
+          isAlgebra x = IsCommAlgebra.isAlgebra (CommAlgebraStr.isCommAlgebra cstr)
 
   CommAlgebra→Algebra : (A : CommAlgebra R ℓ') → Algebra (CommRing→Ring R) ℓ'
-  CommAlgebra→Algebra (_ , str) = (_ , CommAlgebraStr→AlgebraStr str)
+  fst (CommAlgebra→Algebra A) = fst A
+  snd (CommAlgebra→Algebra A) = CommAlgebraStr→AlgebraStr (snd A)
 
   CommAlgebra→CommRing : (A : CommAlgebra R ℓ') → CommRing ℓ'
-  CommAlgebra→CommRing (_ , commalgebrastr  _ _ _ _ _ _ (iscommalgebra isAlgebra ·-comm)) =
-    _ , commringstr _ _ _ _ _ (iscommring (IsAlgebra.isRing isAlgebra) ·-comm)
+  CommAlgebra→CommRing (A , str) = x
+    where open CommRingStr
+          open CommAlgebraStr
+          x : CommRing _
+          fst x = A
+          0r (snd x) = _
+          1r (snd x) = _
+          _+_ (snd x) = _
+          _·_ (snd x) = _
+          - snd x = _
+          IsCommRing.isRing (isCommRing (snd x)) = RingStr.isRing (Algebra→Ring (_ , CommAlgebraStr→AlgebraStr str) .snd)
+          IsCommRing.·Comm (isCommRing (snd x)) = CommAlgebraStr.·Comm  str
 
   module _
       {A : Type ℓ'} {0a 1a : A}
@@ -124,6 +143,22 @@ module _ {R : CommRing ℓ} where
                        x · (r ⋆ y) ∎
     makeIsCommAlgebra .IsCommAlgebra.·Comm = ·Comm
 
+  makeCommAlgebraStr :
+    (A : Type ℓ') (0a 1a : A)
+    (_+_ _·_ : A → A → A) ( -_ : A → A) (_⋆_ : ⟨ R ⟩ → A → A)
+    (isCommAlg : IsCommAlgebra R 0a 1a _+_ _·_ -_ _⋆_)
+    → CommAlgebraStr R A
+  makeCommAlgebraStr A 0a 1a _+_ _·_ -_ _⋆_ isCommAlg =
+    record
+      { 0a = 0a
+      ; 1a = 1a
+      ; _+_ = _+_
+      ; _·_ = _·_
+      ; -_ =  -_
+      ; _⋆_ = _⋆_
+      ; isCommAlgebra = isCommAlg
+      }
+
   module _ (S : CommRing ℓ') where
     open CommRingStr (snd S) renaming (1r to 1S)
     open CommRingStr (snd R) using () renaming (_·_ to _·R_; _+_ to _+R_; 1r to 1R)
@@ -207,9 +242,9 @@ module _ {R : CommRing ℓ} where
                            → (fPres1 : f 1a ≡ 1a)
                            → (fPres+ : (x y : fst M) → f (x + y) ≡ f x + f y)
                            → (fPres· : (x y : fst M) → f (x · y) ≡ f x · f y)
-                           → (fPres⋆ : (r : fst R) (x : fst M) → f (r ⋆ x) ≡ r ⋆ f x)
+                           → (fPres⋆1a : (r : fst R) → f (r ⋆ 1a) ≡ r ⋆ 1a)
                            → CommAlgebraHom M N
-    makeCommAlgebraHom f fPres1 fPres+ fPres· fPres⋆ = f , isHom
+    makeCommAlgebraHom f fPres1 fPres+ fPres· fPres⋆1a = f , isHom
       where fPres0 =
                     f 0a                  ≡⟨ sym (+IdR _) ⟩
                     f 0a + 0a             ≡⟨ cong (λ u → f 0a + u) (sym (+InvR (f 0a))) ⟩
@@ -232,7 +267,14 @@ module _ {R : CommRing ℓ} where
                                (f ((- x) + x) - f x) ≡⟨ cong (λ u → f u - f x) (+InvL x) ⟩
                                (f 0a - f x) ≡⟨ cong (λ u → u - f x) fPres0 ⟩
                                (0a - f x) ≡⟨ +IdL _ ⟩ (- f x) ∎)
-            pres⋆ isHom = fPres⋆
+            pres⋆ isHom r y =
+              f (r ⋆ y)         ≡⟨ cong f (cong (r ⋆_) (sym (·IdL y))) ⟩
+              f (r ⋆ (1a · y))  ≡⟨ cong f (sym (⋆AssocL r 1a y)) ⟩
+              f ((r ⋆ 1a) · y)  ≡⟨ fPres· (r ⋆ 1a) y ⟩
+              f (r ⋆ 1a) · f y  ≡⟨ cong (_· f y) (fPres⋆1a r) ⟩
+              (r ⋆ 1a) · f y    ≡⟨ ⋆AssocL r 1a (f y) ⟩
+              r ⋆ (1a · f y)    ≡⟨ cong (r ⋆_) (·IdL (f y)) ⟩
+              r ⋆ f y           ∎
 
     isPropIsCommAlgebraHom : (f : fst M → fst N) → isProp (IsCommAlgebraHom (snd M) f (snd N))
     isPropIsCommAlgebraHom f = isPropIsAlgebraHom
@@ -253,7 +295,7 @@ isPropIsCommAlgebra R _ _ _ _ _ _ =
       (λ alg → isPropΠ2 λ _ _ → alg .IsAlgebra.is-set _ _))
 
 𝒮ᴰ-CommAlgebra : (R : CommRing ℓ) → DUARel (𝒮-Univ ℓ') (CommAlgebraStr R) (ℓ-max ℓ ℓ')
-𝒮ᴰ-CommAlgebra R =
+𝒮ᴰ-CommAlgebra {ℓ' = ℓ'} R =
   𝒮ᴰ-Record (𝒮-Univ _) (IsCommAlgebraEquiv {R = R})
     (fields:
       data[ 0a ∣ nul ∣ pres0 ]
@@ -262,7 +304,16 @@ isPropIsCommAlgebra R _ _ _ _ _ _ =
       data[ _·_ ∣ bin ∣ pres· ]
       data[ -_ ∣ autoDUARel _ _ ∣ pres- ]
       data[ _⋆_ ∣ autoDUARel _ _ ∣ pres⋆ ]
-      prop[ isCommAlgebra ∣ (λ _ _ → isPropIsCommAlgebra _ _ _ _ _ _ _) ])
+      prop[ isCommAlgebra ∣ (λ A ΣA
+                               → isPropIsCommAlgebra
+                                 {ℓ' = ℓ'}
+                                 R
+                                 (snd (fst (fst (fst (fst (fst ΣA))))))
+                                 (snd (fst (fst (fst (fst ΣA)))))
+                                 (snd (fst (fst (fst ΣA))))
+                                 (snd (fst (fst ΣA)))
+                                 (snd (fst ΣA))
+                                 (snd ΣA)) ])
   where
   open CommAlgebraStr
   open IsAlgebraHom
@@ -279,4 +330,3 @@ uaCommAlgebra {R = R} {A = A} {B = B} = equivFun (CommAlgebraPath R A B)
 
 isGroupoidCommAlgebra : {R : CommRing ℓ} → isGroupoid (CommAlgebra R ℓ')
 isGroupoidCommAlgebra A B = isOfHLevelRespectEquiv 2 (CommAlgebraPath _ _ _) (isSetAlgebraEquiv _ _)
--- -}
diff --git a/Cubical/Algebra/CommAlgebra/FPAlgebra/Base.agda b/Cubical/Algebra/CommAlgebra/FPAlgebra/Base.agda
index 229c8cb20a..322e06a5f9 100644
--- a/Cubical/Algebra/CommAlgebra/FPAlgebra/Base.agda
+++ b/Cubical/Algebra/CommAlgebra/FPAlgebra/Base.agda
@@ -51,7 +51,7 @@ module _ {R : CommRing ℓ} where
   evPolyHomomorphic A B f P values =
     (fst f) (evPoly A P values)                         ≡⟨ refl ⟩
     (fst f) (fst (freeInducedHom A values) P)           ≡⟨ refl ⟩
-    fst (f ∘a freeInducedHom A values) P                ≡⟨ cong (λ u → fst u P) (natIndHomR f values) ⟩
+    fst (f ∘a freeInducedHom A values) P                ≡⟨ cong (λ u → fst u P) (natIndHomR {A = A} {B = B} f values) ⟩
     fst (freeInducedHom B (fst f ∘ values)) P           ≡⟨ refl ⟩
     evPoly B P (fst f ∘ values) ∎
     where open AlgebraHoms
diff --git a/Cubical/Algebra/CommAlgebra/FPAlgebra/Instances.agda b/Cubical/Algebra/CommAlgebra/FPAlgebra/Instances.agda
index 26e21cad66..24319606d8 100644
--- a/Cubical/Algebra/CommAlgebra/FPAlgebra/Instances.agda
+++ b/Cubical/Algebra/CommAlgebra/FPAlgebra/Instances.agda
@@ -78,13 +78,13 @@ module _ (R : CommRing ℓ) where
         inverse1 : fromA ∘a toA ≡ idAlgebraHom _
         inverse1 =
           fromA ∘a toA
-            ≡⟨ sym (unique _ _ _ _ _ _ (λ i → cong (fst fromA) (
+            ≡⟨ sym (unique _ _ B _ _ _ (λ i → cong (fst fromA) (
                  fst toA (generator n emptyGen i)
                    ≡⟨ inducedHomOnGenerators _ _ _ _ _ _ ⟩
                  Construction.var i
                    ∎))) ⟩
           inducedHom n emptyGen B (generator _ _) (relationsHold _ _)
-            ≡⟨ unique _ _ _ _ _ _ (λ i → refl) ⟩
+            ≡⟨ unique _ _ B _ _ _ (λ i → refl) ⟩
           idAlgebraHom _
             ∎
         inverse2 : toA ∘a fromA ≡ idAlgebraHom _
diff --git a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Base.agda b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Base.agda
index b66cd0433f..e8bbde5477 100644
--- a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Base.agda
+++ b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Base.agda
@@ -19,6 +19,7 @@ module Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base where
   For more, see the Properties file.
 -}
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure using (⟨_⟩)
 
 open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.CommAlgebra.Base
@@ -90,7 +91,25 @@ module Construction (R : CommRing ℓ) where
                                     ·-assoc ·-lid ldist ·-comm
                                     ⋆-assoc ⋆-rdist-+ ⋆-ldist-+ ·-lid ⋆-assoc-·
 
-_[_] : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R (ℓ-max ℓ ℓ')
-(R [ I ]) = R[ I ] , commalgebrastr 0a 1a _+_ _·_ -_ _⋆_ isCommAlgebra
-  where
+
+
+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
+  var : {R : CommRing ℓ} {I : Type ℓ'} → I → ⟨ R [ I ] ⟩
+  var = Construction.var
diff --git a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/OnCoproduct.agda b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/OnCoproduct.agda
index a20195fca7..7c25d17c79 100644
--- a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/OnCoproduct.agda
+++ b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/OnCoproduct.agda
@@ -13,9 +13,8 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Equiv.BiInvertible
 open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Structure using (⟨_⟩; str)
 open import Cubical.Foundations.GroupoidLaws
-open import Cubical.Foundations.Structure
 
 open import Cubical.Data.Sum as ⊎
 open import Cubical.Data.Sigma
@@ -30,9 +29,62 @@ private variable
     ℓ ℓ' : Level
 
 module CalculateFreeCommAlgebraOnCoproduct (R : CommRing ℓ) (I J : Type ℓ) where
-  open Construction using (var; const)
   open CommAlgebraStr ⦃...⦄
 
+  R[I⊎J] : CommAlgebra R ℓ
+  R[I⊎J] = R [ I ⊎ J ]
+
+  R[I]→R[I⊎J] : CommAlgebraHom (R [ I ]) R[I⊎J]
+  R[I]→R[I⊎J] = inducedHom (R [ I ⊎ J ]) (λ i → var (inl i))
+
+  R[I]AsRing : CommRing ℓ
+  R[I]AsRing = CommAlgebra→CommRing (R [ I ])
+
+  R[I⊎J]overR[I] : CommAlgebra R[I]AsRing ℓ
+  R[I⊎J]overR[I] = Iso.inv (CommAlgChar.CommAlgIso (CommAlgebra→CommRing (R [ I ])))
+                   (CommAlgebra→CommRing (R [ I ⊎ J ]) ,
+                    (CommAlgebraHom→CommRingHom (R [ I ]) (R [ I ⊎ J ]) R[I]→R[I⊎J]))
+
+  module UniversalPropertyOfR[I⊎J]overR[I]
+    (A : CommAlgebra R[I]AsRing ℓ)
+    (φ : J → ⟨ A ⟩)
+    where
+
+    private instance
+      _ : CommAlgebraStr R[I]AsRing ⟨ A ⟩
+      _ = str A
+
+    AOverR : CommAlgebra R ℓ
+    AOverR = (baseChange baseRingHom A)
+
+    _ : Type ℓ
+    _ = CommAlgebraHom R[I⊎J] (baseChange baseRingHom A)
+
+    inducedHomOverR : CommAlgebraHom R[I⊎J] AOverR
+    inducedHomOverR = inducedHom AOverR (⊎.rec (λ i → var i ⋆ 1a) φ)
+
+    inducedHomOverR[I] : CommAlgebraHom R[I⊎J]overR[I] A
+    fst inducedHomOverR[I] = fst inducedHomOverR
+    snd inducedHomOverR[I] = record
+                              { pres0 = homStr .pres0
+                              ; pres1 = homStr .pres1
+                              ; pres+ = homStr .pres+
+                              ; pres· = homStr .pres·
+                              ; pres- = homStr .pres-
+                              ; pres⋆ = λ r x → f (r ⋆ x) ≡⟨ {!!} ⟩
+                                                r ⋆ f x ∎
+                              }
+        where open IsAlgebraHom
+              homStr = inducedHomOverR .snd
+              f = inducedHomOverR .fst
+              instance
+                _ = R[I⊎J]overR[I] .snd
+                _ = A .snd
+
+--  (r : R[I]) → (y : R[I⊎J]) → f (r ⋆ 1a) ≡ r ⋆ 1a
+--  (r : R[I]) → (y : R[I⊎J]) → f (var (inl i)) ≡ var i ⋆ 1a
+
+{-
   {-
      We start by defining R[I][J] and R[I⊎J] as R[I] algebras,
      which we need later to use universal properties
@@ -71,14 +123,22 @@ module CalculateFreeCommAlgebraOnCoproduct (R : CommRing ℓ) (I J : Type ℓ) w
                   (⊎.rec (λ i → const (var i))
                          λ j → var j)
 
+  isoR : Iso (CommAlgebra R ℓ) (CommAlgChar.CommRingWithHom R)
   isoR = CommAlgChar.CommAlgIso R
+
+  isoR[I] : Iso (CommAlgebra (CommAlgebra→CommRing (R [ I ])) ℓ)
+                (CommAlgChar.CommRingWithHom (CommAlgebra→CommRing (R [ I ])))
   isoR[I] = CommAlgChar.CommAlgIso (CommAlgebra→CommRing (R [ I ]))
+
+  asHomOverR[I] : CommAlgChar.CommRingWithHom (CommAlgebra→CommRing (R [ I ]))
   asHomOverR[I] = Iso.fun isoR[I] R[I⊎J]overR[I]
+
+  asHomOverR : CommAlgChar.CommRingWithHom R
   asHomOverR = Iso.fun isoR (R [ I ⊎ J ])
 
   ≡RingHoms : snd asHomOverR[I] ∘r baseRingHom ≡ baseRingHom
   ≡RingHoms =
-    RingHom≡
+    {!RingHom≡
       (funExt λ x →
         fst (snd asHomOverR[I] ∘r baseRingHom) x ≡⟨⟩
         fst (snd asHomOverR[I]) (const x · 1a)   ≡⟨⟩
@@ -86,7 +146,7 @@ module CalculateFreeCommAlgebraOnCoproduct (R : CommRing ℓ) (I J : Type ℓ) w
         const x ⋆ 1a                             ≡⟨⟩
         (fst ψ (const x)) · 1a                   ≡⟨⟩
         (const x · const 1r) · 1a                ≡⟨ cong (_· 1a) (·IdR (const x)) ⟩
-        const x · 1a ∎)
+        const x · 1a ∎)!}
 
   ≡R[I⊎J] =
     baseChange baseRingHom R[I⊎J]overR[I]                                                     ≡⟨⟩
@@ -256,3 +316,4 @@ module _ {R : CommRing ℓ} {I J : Type ℓ} where
       invr-rightInv asBiInv = toFromOverR[I]
       invl asBiInv = fst from
       invl-leftInv asBiInv = fromTo
+-- -}
diff --git a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda
index a7dea81c7c..43e8e37396 100644
--- a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda
+++ b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda
@@ -48,8 +48,13 @@ module Theory {R : CommRing ℓ} {I : Type ℓ'} where
          using (0r; 1r)
          renaming (_·_ to _·r_; _+_ to _+r_; ·Comm to ·r-comm; ·IdR to ·r-rid)
 
+  open CommAlgebraStr ⦃...⦄
+
+  private instance
+    _ : CommAlgebraStr R ⟨ R [ I ] ⟩
+    _ = str (R [ I ])
+
   module C = Construction
-  open C using (var; const)
 
   {-
     Construction of the 'elimProp' eliminator.
@@ -59,14 +64,17 @@ module Theory {R : CommRing ℓ} {I : Type ℓ'} where
     (isPropP : {x : _} → isProp (P x))
     (onVar : {x : I} → P (var x))
     (onConst : {r : ⟨ R ⟩} → P (const r))
-    (on+ : {x y : ⟨ R [ I ] ⟩} → P x → P y → P (x C.+ y))
-    (on· : {x y : ⟨ R [ I ] ⟩} → P x → P y → P (x C.· y))
+    (on+ : {x y : ⟨ R [ I ] ⟩} → P x → P y → P (x + y))
+    (on· : {x y : ⟨ R [ I ] ⟩} → P x → P y → P (x · y))
     where
 
     private
-      on- : {x : ⟨ R [ I ] ⟩} → P x → P (C.- x)
-      on- {x} Px = subst P (minusByMult x) (on· onConst Px)
-        where open ModuleTheory _ (Algebra→Module (CommAlgebra→Algebra (R [ I ])))
+      opaque
+        unfolding const freeCAlgStr
+
+        on- : {x : ⟨ R [ I ] ⟩} → P x → P (- x)
+        on- {x} Px = subst P (minusByMult x) (on· onConst Px)
+          where open ModuleTheory _ (Algebra→Module (CommAlgebra→Algebra (R [ I ])))
 
       -- A helper to deal with the path constructor cases.
       mkPathP :
@@ -77,202 +85,229 @@ module Theory {R : CommRing ℓ} {I : Type ℓ'} where
         PathP (λ i → P (p i)) Px0 Px1
       mkPathP _ = isProp→PathP λ i → isPropP
 
-    elimProp : ((x : _) → P x)
-
-    elimProp (var _) = onVar
-    elimProp (const _) = onConst
-    elimProp (x C.+ y) = on+ (elimProp x) (elimProp y)
-    elimProp (C.- x) = on- (elimProp x)
-    elimProp (x C.· y) = on· (elimProp x) (elimProp y)
-
-    elimProp (C.+-assoc x y z i) =
-      mkPathP (C.+-assoc x y z)
-        (on+ (elimProp x) (on+ (elimProp y) (elimProp z)))
-        (on+ (on+ (elimProp x) (elimProp y)) (elimProp z))
-        i
-    elimProp (C.+-rid x i) =
-      mkPathP (C.+-rid x)
-        (on+ (elimProp x) onConst)
-        (elimProp x)
-        i
-    elimProp (C.+-rinv x i) =
-      mkPathP (C.+-rinv x)
-        (on+ (elimProp x) (on- (elimProp x)))
-        onConst
-        i
-    elimProp (C.+-comm x y i) =
-      mkPathP (C.+-comm x y)
-        (on+ (elimProp x) (elimProp y))
-        (on+ (elimProp y) (elimProp x))
-        i
-    elimProp (C.·-assoc x y z i) =
-      mkPathP (C.·-assoc x y z)
-        (on· (elimProp x) (on· (elimProp y) (elimProp z)))
-        (on· (on· (elimProp x) (elimProp y)) (elimProp z))
-        i
-    elimProp (C.·-lid x i) =
-      mkPathP (C.·-lid x)
-        (on· onConst (elimProp x))
-        (elimProp x)
-        i
-    elimProp (C.·-comm x y i) =
-      mkPathP (C.·-comm x y)
-        (on· (elimProp x) (elimProp y))
-        (on· (elimProp y) (elimProp x))
-        i
-    elimProp (C.ldist x y z i) =
-      mkPathP (C.ldist x y z)
-        (on· (on+ (elimProp x) (elimProp y)) (elimProp z))
-        (on+ (on· (elimProp x) (elimProp z)) (on· (elimProp y) (elimProp z)))
-        i
-    elimProp (C.+HomConst s t i) =
-      mkPathP (C.+HomConst s t)
-        onConst
-        (on+ onConst onConst)
-        i
-    elimProp (C.·HomConst s t i) =
-      mkPathP (C.·HomConst s t)
-        onConst
-        (on· onConst onConst)
-        i
-
-    elimProp (C.0-trunc x y p q i j) =
-      isOfHLevel→isOfHLevelDep 2 (λ _ → isProp→isSet isPropP)
-        (elimProp x)
-        (elimProp y)
-        (cong elimProp p)
-        (cong elimProp q)
-        (C.0-trunc x y p q)
-        i
-        j
+    opaque
+      unfolding var const freeCAlgStr
+
+      elimProp : ((x : _) → P x)
+
+      elimProp (C.var _) = onVar
+      elimProp (C.const _) = onConst
+      elimProp (x C.+ y) = on+ (elimProp x) (elimProp y)
+      elimProp (C.- x) = on- (elimProp x)
+      elimProp (x C.· y) = on· (elimProp x) (elimProp y)
+
+      elimProp (C.+-assoc x y z i) =
+        mkPathP (C.+-assoc x y z)
+          (on+ (elimProp x) (on+ (elimProp y) (elimProp z)))
+          (on+ (on+ (elimProp x) (elimProp y)) (elimProp z))
+          i
+      elimProp (C.+-rid x i) =
+        mkPathP (C.+-rid x)
+          (on+ (elimProp x) onConst)
+          (elimProp x)
+          i
+      elimProp (C.+-rinv x i) =
+        mkPathP (C.+-rinv x)
+          (on+ (elimProp x) (on- (elimProp x)))
+          onConst
+          i
+      elimProp (C.+-comm x y i) =
+        mkPathP (C.+-comm x y)
+          (on+ (elimProp x) (elimProp y))
+          (on+ (elimProp y) (elimProp x))
+          i
+      elimProp (C.·-assoc x y z i) =
+        mkPathP (C.·-assoc x y z)
+          (on· (elimProp x) (on· (elimProp y) (elimProp z)))
+          (on· (on· (elimProp x) (elimProp y)) (elimProp z))
+          i
+      elimProp (C.·-lid x i) =
+        mkPathP (C.·-lid x)
+          (on· onConst (elimProp x))
+          (elimProp x)
+          i
+      elimProp (C.·-comm x y i) =
+        mkPathP (C.·-comm x y)
+          (on· (elimProp x) (elimProp y))
+          (on· (elimProp y) (elimProp x))
+          i
+      elimProp (C.ldist x y z i) =
+        mkPathP (C.ldist x y z)
+          (on· (on+ (elimProp x) (elimProp y)) (elimProp z))
+          (on+ (on· (elimProp x) (elimProp z)) (on· (elimProp y) (elimProp z)))
+          i
+      elimProp (C.+HomConst s t i) =
+        mkPathP (C.+HomConst s t)
+          onConst
+          (on+ onConst onConst)
+          i
+      elimProp (C.·HomConst s t i) =
+        mkPathP (C.·HomConst s t)
+          onConst
+          (on· onConst onConst)
+          i
+
+      elimProp (C.0-trunc x y p q i j) =
+        isOfHLevel→isOfHLevelDep 2 (λ _ → isProp→isSet isPropP)
+          (elimProp x)
+          (elimProp y)
+          (cong elimProp p)
+          (cong elimProp q)
+          (C.0-trunc x y p q)
+          i
+          j
 
   {-
     Construction of the induced map.
   -}
   module _ (A : CommAlgebra R ℓ'') (φ : I → ⟨ A ⟩) where
-    open CommAlgebraStr (A .snd)
+
+    private instance
+      _ : CommAlgebraStr R ⟨ A ⟩
+      _ = str A
+
     open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra A)
 
-    imageOf0Works : 0r ⋆ 1a ≡ 0a
-    imageOf0Works = ⋆AnnihilL 1a
-
-    imageOf1Works : 1r ⋆ 1a ≡ 1a
-    imageOf1Works = ⋆IdL 1a
-
-    inducedMap : ⟨ R [ I ] ⟩ → ⟨ A ⟩
-    inducedMap (var x) = φ x
-    inducedMap (const r) = r ⋆ 1a
-    inducedMap (P C.+ Q) = (inducedMap P) + (inducedMap Q)
-    inducedMap (C.- P) = - inducedMap P
-    inducedMap (C.+-assoc P Q S i) = +Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i
-    inducedMap (C.+-rid P i) =
-      let
-        eq : (inducedMap P) + (inducedMap (const 0r)) ≡ (inducedMap P)
-        eq = (inducedMap P) + (inducedMap (const 0r)) ≡⟨ refl ⟩
-             (inducedMap P) + (0r ⋆ 1a)               ≡⟨ cong
-                                                         (λ u → (inducedMap P) + u)
-                                                         (imageOf0Works) ⟩
-             (inducedMap P) + 0a                      ≡⟨ +IdR _ ⟩
-             (inducedMap P) ∎
-      in eq i
-    inducedMap (C.+-rinv P i) =
-      let eq : (inducedMap P - inducedMap P) ≡ (inducedMap (const 0r))
-          eq = (inducedMap P - inducedMap P) ≡⟨ +InvR _ ⟩
-               0a                            ≡⟨ sym imageOf0Works ⟩
-               (inducedMap (const 0r))∎
-      in eq i
-    inducedMap (C.+-comm P Q i) = +Comm (inducedMap P) (inducedMap Q) i
-    inducedMap (P C.· Q) = inducedMap P · inducedMap Q
-    inducedMap (C.·-assoc P Q S i) = ·Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i
-    inducedMap (C.·-lid P i) =
-      let eq = inducedMap (const 1r) · inducedMap P ≡⟨ cong (λ u → u · inducedMap P) imageOf1Works ⟩
-               1a · inducedMap P                    ≡⟨ ·IdL (inducedMap P) ⟩
-               inducedMap P ∎
-      in eq i
-    inducedMap (C.·-comm P Q i) = ·Comm (inducedMap P) (inducedMap Q) i
-    inducedMap (C.ldist P Q S i) = ·DistL+ (inducedMap P) (inducedMap Q) (inducedMap S) i
-    inducedMap (C.+HomConst s t i) = ⋆DistL+ s t 1a i
-    inducedMap (C.·HomConst s t i) =
-      let eq = (s ·r t) ⋆ 1a       ≡⟨ cong (λ u → u ⋆ 1a) (·r-comm _ _) ⟩
-               (t ·r s) ⋆ 1a       ≡⟨ ⋆Assoc t s 1a ⟩
-               t ⋆ (s ⋆ 1a)        ≡⟨ cong (λ u → t ⋆ u) (sym (·IdR _)) ⟩
-               t ⋆ ((s ⋆ 1a) · 1a) ≡⟨ ⋆AssocR t (s ⋆ 1a) 1a ⟩
-               (s ⋆ 1a) · (t ⋆ 1a) ∎
-      in eq i
-    inducedMap (C.0-trunc P Q p q i j) =
-      is-set (inducedMap P) (inducedMap Q) (cong _ p) (cong _ q) i j
+--    imageOf0Works : 0r ⋆ 1a ≡ 0a
+--    imageOf0Works = ⋆AnnihilL 1a
+
+--    imageOf1Works : 1r ⋆ 1a ≡ 1a
+--    imageOf1Works = ⋆IdL 1a
+
+    opaque
+      unfolding const
+
+      inducedMap : ⟨ R [ I ] ⟩ → ⟨ A ⟩
+      inducedMap (C.var x) = φ x
+      inducedMap (C.const r) = r ⋆ 1a
+      inducedMap (P C.+ Q) = (inducedMap P) + (inducedMap Q)
+      inducedMap (C.- P) = - inducedMap P
+      inducedMap (C.+-assoc P Q S i) = +Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i
+      inducedMap (C.+-rid P i) =
+        let
+          eq : (inducedMap P) + (inducedMap (const 0r)) ≡ (inducedMap P)
+          eq = (inducedMap P) + (inducedMap (const 0r)) ≡⟨ refl ⟩
+               (inducedMap P) + (0r ⋆ 1a)               ≡⟨ cong
+                                                           (λ u → (inducedMap P) + u)
+                                                           (⋆AnnihilL 1a) ⟩
+               (inducedMap P) + 0a                      ≡⟨ +IdR _ ⟩
+               (inducedMap P) ∎
+        in eq i
+      inducedMap (C.+-rinv P i) =
+        let eq : (inducedMap P - inducedMap P) ≡ (inducedMap (const 0r))
+            eq = (inducedMap P - inducedMap P) ≡⟨ +InvR _ ⟩
+                 0a                            ≡⟨ sym (⋆AnnihilL 1a) ⟩
+                 (inducedMap (const 0r))∎
+        in eq i
+      inducedMap (C.+-comm P Q i) = +Comm (inducedMap P) (inducedMap Q) i
+      inducedMap (P C.· Q) = inducedMap P · inducedMap Q
+      inducedMap (C.·-assoc P Q S i) = ·Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i
+      inducedMap (C.·-lid P i) =
+        let eq = inducedMap (const 1r) · inducedMap P ≡⟨ cong (λ u → u · inducedMap P) (⋆IdL 1a) ⟩
+                 1a · inducedMap P                    ≡⟨ ·IdL (inducedMap P) ⟩
+                 inducedMap P ∎
+        in eq i
+      inducedMap (C.·-comm P Q i) = ·Comm (inducedMap P) (inducedMap Q) i
+      inducedMap (C.ldist P Q S i) = ·DistL+ (inducedMap P) (inducedMap Q) (inducedMap S) i
+      inducedMap (C.+HomConst s t i) = ⋆DistL+ s t 1a i
+      inducedMap (C.·HomConst s t i) =
+        let eq = (s ·r t) ⋆ 1a       ≡⟨ cong (λ u → u ⋆ 1a) (·r-comm _ _) ⟩
+                 (t ·r s) ⋆ 1a       ≡⟨ ⋆Assoc t s 1a ⟩
+                 t ⋆ (s ⋆ 1a)        ≡⟨ cong (λ u → t ⋆ u) (sym (·IdR _)) ⟩
+                 t ⋆ ((s ⋆ 1a) · 1a) ≡⟨ ⋆AssocR t (s ⋆ 1a) 1a ⟩
+                 (s ⋆ 1a) · (t ⋆ 1a) ∎
+        in eq i
+      inducedMap (C.0-trunc P Q p q i j) =
+        is-set (inducedMap P) (inducedMap Q) (cong _ p) (cong _ q) i j
 
     module _ where
       open IsAlgebraHom
 
-      inducedHom : CommAlgebraHom (R [ I ]) A
-      inducedHom .fst = inducedMap
-      inducedHom .snd .pres0 = ⋆AnnihilL _
-      inducedHom .snd .pres1 = imageOf1Works
-      inducedHom .snd .pres+ x y = refl
-      inducedHom .snd .pres· x y = refl
-      inducedHom .snd .pres- x = refl
-      inducedHom .snd .pres⋆ r x =
-        (r ⋆ 1a) · inducedMap x ≡⟨ ⋆AssocL r 1a (inducedMap x) ⟩
-        r ⋆ (1a · inducedMap x) ≡⟨ cong (λ u → r ⋆ u) (·IdL (inducedMap x)) ⟩
-        r ⋆ inducedMap x ∎
+      opaque
+        unfolding inducedMap freeCAlgStr
+
+        inducedHom : CommAlgebraHom (R [ I ]) A
+        inducedHom .fst = inducedMap
+        inducedHom .snd .pres0 = ⋆AnnihilL _
+        inducedHom .snd .pres1 = ⋆IdL 1a
+        inducedHom .snd .pres+ x y = refl
+        inducedHom .snd .pres· x y = refl
+        inducedHom .snd .pres- x = refl
+        inducedHom .snd .pres⋆ r x =
+          (r ⋆ 1a) · inducedMap x ≡⟨ ⋆AssocL r 1a (inducedMap x) ⟩
+          r ⋆ (1a · inducedMap x) ≡⟨ cong (λ u → r ⋆ u) (·IdL (inducedMap x)) ⟩
+          r ⋆ inducedMap x ∎
 
   module _ (A : CommAlgebra R ℓ'') where
-    open CommAlgebraStr (A .snd)
+
+    private instance
+      _ : CommAlgebraStr R ⟨ A ⟩
+      _ = str A
+
     open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra A)
 
-    Hom = CommAlgebraHom  (R [ I ]) A
+    Hom = CommAlgebraHom (R [ I ]) A
     open IsAlgebraHom
 
     evaluateAt : Hom → I → ⟨ A ⟩
     evaluateAt φ x = φ .fst (var x)
 
-    mapRetrievable : ∀ (φ : I → ⟨ A ⟩)
-                     → evaluateAt (inducedHom A φ) ≡ φ
-    mapRetrievable φ = refl
-
-    homRetrievable : ∀ (f : Hom)
-                     → inducedMap A (evaluateAt f) ≡ fst f
-    homRetrievable f = funExt (
-      elimProp
-        {P = λ x → ι x ≡ f $a x}
-        (is-set _ _)
-        (λ {x} → refl)
-        (λ {r} →
-          r ⋆ 1a                      ≡⟨ cong (λ u → r ⋆ u) (sym f.pres1) ⟩
-          r ⋆ (f $a (const 1r))       ≡⟨ sym (f.pres⋆ r _) ⟩
-          f $a (const r C.· const 1r) ≡⟨ cong (λ u → f $a u) (sym (C.·HomConst r 1r)) ⟩
-          f $a (const (r ·r 1r))      ≡⟨ cong (λ u → f $a (const u)) (·r-rid r) ⟩
-          f $a (const r) ∎)
-
-        (λ {x} {y} eq-x eq-y →
-          ι (x C.+ y)           ≡⟨ refl ⟩
-          (ι x + ι y)           ≡⟨ cong (λ u → u + ι y) eq-x ⟩
-          ((f $a x) + ι y)      ≡⟨ cong (λ u → (f $a x) + u) eq-y ⟩
-          ((f $a x) + (f $a y)) ≡⟨ sym (f.pres+ _ _) ⟩
-          (f $a (x C.+ y)) ∎)
-
-        (λ {x} {y} eq-x eq-y →
-          ι (x C.· y)         ≡⟨ refl ⟩
-          ι x     · ι y       ≡⟨ cong (λ u → u · ι y) eq-x ⟩
-          (f $a x) · (ι y)    ≡⟨ cong (λ u → (f $a x) · u) eq-y ⟩
-          (f $a x) · (f $a y) ≡⟨ sym (f.pres· _ _) ⟩
-          f $a (x C.· y) ∎)
-      )
-      where
-      ι = inducedMap A (evaluateAt f)
-      module f = IsAlgebraHom (f .snd)
+    opaque
+      unfolding inducedHom var
+
+      mapRetrievable : ∀ (φ : I → ⟨ A ⟩)
+                       → evaluateAt (inducedHom A φ) ≡ φ
+      mapRetrievable φ = refl
+
+    opaque
+      unfolding inducedHom const var
+
+      homRetrievable : ∀ (f : Hom)
+                       → inducedHom A (evaluateAt f) ≡ f
+      homRetrievable f =
+        Σ≡Prop
+          (isPropIsCommAlgebraHom {M = R [ I ]} {N = A})
+          (funExt (
+            elimProp
+              {P = λ x → ι x ≡ f $a x}
+              (is-set _ _)
+              (λ {x} → refl)
+              (λ {r} →
+                r ⋆ 1a                      ≡⟨ cong (λ u → r ⋆ u) (sym f.pres1) ⟩
+                r ⋆ (f $a (const 1r))       ≡⟨ sym (f.pres⋆ r _) ⟩
+                f $a (const r C.· const 1r) ≡⟨ cong (λ u → f $a u) (sym (C.·HomConst r 1r)) ⟩
+                f $a (const (r ·r 1r))      ≡⟨ cong (λ u → f $a (const u)) (·r-rid r) ⟩
+                f $a (const r) ∎)
+
+              (λ {x} {y} eq-x eq-y →
+                ι (x C.+ y)           ≡⟨ refl ⟩
+                (ι x + ι y)           ≡⟨ cong (λ u → u + ι y) eq-x ⟩
+                ((f $a x) + ι y)      ≡⟨ cong (λ u → (f $a x) + u) eq-y ⟩
+                ((f $a x) + (f $a y)) ≡⟨ sym (f.pres+ _ _) ⟩
+                (f $a (x C.+ y)) ∎)
+
+              λ {x} {y} eq-x eq-y →
+                ι (x C.· y)         ≡⟨ refl ⟩
+                ι x     · ι y       ≡⟨ cong (λ u → u · ι y) eq-x ⟩
+                (f $a x) · (ι y)    ≡⟨ cong (λ u → (f $a x) · u) eq-y ⟩
+                (f $a x) · (f $a y) ≡⟨ sym (f.pres· _ _) ⟩
+                f $a (x C.· y) ∎
+            ))
+        where
+        ι : ⟨ R [ I ] ⟩ → ⟨ A ⟩
+        ι = inducedMap A (evaluateAt f)
+        module f = IsAlgebraHom (f .snd)
 
 
 evaluateAt : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'')
              (f : CommAlgebraHom (R [ I ]) A)
              → (I → fst A)
-evaluateAt A f x = f $a (Construction.var x)
+evaluateAt A f x = f $a (var x)
 
 inducedHom : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'')
              (φ : I → fst A )
              → CommAlgebraHom (R [ I ]) A
-inducedHom A φ = Theory.inducedHom A φ
+inducedHom = Theory.inducedHom
 
 
 homMapIso : {R : CommRing ℓ} {I : Type ℓ''} (A : CommAlgebra R ℓ')
@@ -280,16 +315,17 @@ homMapIso : {R : CommRing ℓ} {I : Type ℓ''} (A : CommAlgebra R ℓ')
 Iso.fun (homMapIso A) = evaluateAt A
 Iso.inv (homMapIso A) = inducedHom A
 Iso.rightInv (homMapIso A) = λ ϕ → Theory.mapRetrievable A ϕ
-Iso.leftInv (homMapIso {R = R} {I = I} A) =
-  λ f → Σ≡Prop (λ f → isPropIsCommAlgebraHom {M = R [ I ]} {N = A} f)
-               (Theory.homRetrievable A f)
+Iso.leftInv (homMapIso {R = R} {I = I} A) = Theory.homRetrievable A
 
 inducedHomUnique :
   {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'') (φ : I → fst A )
-  → (f : CommAlgebraHom (R [ I ]) A) → ((i : I) → fst f (Construction.var i) ≡ φ i)
+  → (f : CommAlgebraHom (R [ I ]) A) → ((i : I) → evaluateAt A f i ≡ φ i)
   → f ≡ inducedHom A φ
 inducedHomUnique {I = I} A φ f p =
-  isoFunInjective (homMapIso A) f (inducedHom A φ) λ j i → p i j
+  isoFunInjective (homMapIso A) f (inducedHom A φ) (
+    evaluateAt A f                 ≡⟨ funExt p ⟩
+    φ                              ≡⟨ sym (Theory.mapRetrievable A φ) ⟩
+    evaluateAt A (inducedHom A φ)  ∎)
 
 homMapPath : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R (ℓ-max ℓ ℓ'))
              → CommAlgebraHom (R [ I ]) A ≡ (I → fst A)
@@ -299,7 +335,7 @@ homMapPath A = isoToPath (homMapIso A)
 equalByUMP : {R : CommRing ℓ} {I : Type ℓ'}
            → (A : CommAlgebra R ℓ'')
            → (f g : CommAlgebraHom (R [ I ]) A)
-           → ((i : I) → fst f (Construction.var i) ≡ fst g (Construction.var i))
+           → ((i : I) → fst f (var i) ≡ fst g (var i))
            → (x : ⟨ R [ I ] ⟩) → fst f x ≡ fst g x
 equalByUMP {R = R} {I = I} A f g = funExt⁻ ∘ cong fst ∘ isoFunInjective (homMapIso A) f g ∘ funExt
 
@@ -307,14 +343,14 @@ equalByUMP {R = R} {I = I} A f g = funExt⁻ ∘ cong fst ∘ isoFunInjective (h
    algebras with the same universal property -}
 isIdByUMP : {R : CommRing ℓ} {I : Type ℓ'}
           → (f : CommAlgebraHom (R [ I ]) (R [ I ]))
-          → ((i : I) → fst f (Construction.var i) ≡ Construction.var i)
+          → ((i : I) → fst f (var i) ≡ var i)
           → (x : ⟨ R [ I ] ⟩) → fst f x ≡ x
 isIdByUMP {R = R} {I = I} f p = equalByUMP (R [ I ]) f (idCAlgHom (R [ I ])) p
 
 -- The homomorphism induced by the variables is the identity.
 inducedHomVar : (R : CommRing ℓ) (I : Type ℓ')
-              → inducedHom (R [ I ]) Construction.var ≡ idCAlgHom (R [ I ])
-inducedHomVar R I = isoFunInjective (homMapIso (R [ I ])) _ _ refl
+              → inducedHom (R [ I ]) var ≡ idCAlgHom (R [ I ])
+inducedHomVar R I = sym (inducedHomUnique (R [ I ]) var (idCAlgHom (R [ I ])) λ i → refl)
 
 module _ {R : CommRing ℓ} {A B : CommAlgebra R ℓ''} where
   open AlgebraHoms
@@ -342,22 +378,12 @@ module _ {R : CommRing ℓ} {A B : CommAlgebra R ℓ''} where
   natIndHomR : {I : Type ℓ'} (ψ : CommAlgebraHom A B)
                (ϕ : I → ⟨ A ⟩)
                → ψ ∘a inducedHom A ϕ ≡ inducedHom B (fst ψ ∘ ϕ)
-  natIndHomR ψ ϕ = isoFunInjective (homMapIso B) _ _
-                (evaluateAt B (ψ ∘a (inducedHom A ϕ))        ≡⟨ refl ⟩
-                 fst ψ ∘ evaluateAt A (inducedHom A ϕ)       ≡⟨ refl ⟩
-                 fst ψ ∘ ϕ                                   ≡⟨ Iso.rightInv (homMapIso B) _ ⟩
-                 evaluateAt B (inducedHom B (fst ψ ∘ ϕ))     ∎)
-
-  {-
-    Hom(R[I],A) → (I → A)
-         ↓          ↓
-    Hom(R[J],A) → (J → A)
-  -}
-  naturalEvL : {I J : Type ℓ'} (φ : J → I)
-             (f : CommAlgebraHom (R [ I ]) A)
-             → (evaluateAt A f) ∘ φ
-               ≡ evaluateAt A (f ∘a (inducedHom (R [ I ]) (λ x → Construction.var (φ x))))
-  naturalEvL φ f = refl
+  natIndHomR ψ ϕ =
+    isoFunInjective (homMapIso B) _ _ (
+      evaluateAt B (ψ ∘a (inducedHom A ϕ))        ≡⟨ refl ⟩
+      fst ψ ∘ evaluateAt A (inducedHom A ϕ)       ≡⟨ cong (fst ψ ∘_) (Iso.rightInv (homMapIso A) _) ⟩
+      fst ψ ∘ ϕ                                   ≡⟨ sym (Iso.rightInv (homMapIso B) _) ⟩
+      evaluateAt B (inducedHom B (fst ψ ∘ ϕ))     ∎)
 
 module _ {R : CommRing ℓ} where
   {-
@@ -377,9 +403,7 @@ module _ {R : CommRing ℓ} where
                    from = inducedHom B
 
                    from-to : (x : _) → from (to x) ≡ x
-                   from-to x =
-                     Σ≡Prop (λ f → isPropIsCommAlgebraHom {M = R [ ⊥ ]} {N = B} f)
-                            (Theory.homRetrievable B x)
+                   from-to x = Theory.homRetrievable B x
 
                    equiv : CommAlgebraHom (R [ ⊥ ]) B ≃ (⊥ → fst B)
                    equiv =
diff --git a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/UPAsCRing.agda b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/UPAsCRing.agda
new file mode 100644
index 0000000000..445590d087
--- /dev/null
+++ b/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/UPAsCRing.agda
@@ -0,0 +1,42 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.CommAlgebra.FreeCommAlgebra.UPAsCRing where
+{-
+  This file contains
+  * The universal property of the free commutative algebra/polynomial ring
+    as a commutative ring.
+-}
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Function hiding (const)
+open import Cubical.Foundations.Isomorphism
+
+open import Cubical.Data.Sigma.Properties using (Σ≡Prop)
+open import Cubical.HITs.SetTruncation
+
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommAlgebra
+open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base
+open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties
+open import Cubical.Algebra.Algebra
+open import Cubical.Algebra.Module using (module ModuleTheory)
+
+open import Cubical.Data.Empty
+open import Cubical.Data.Sigma
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+
+module UniversalPropertyAsCommRing
+         {R : CommRing ℓ} (I : Type ℓ')
+         (S : CommRing ℓ'') (f : CommRingHom R S)
+         (φ : I → ⟨ S ⟩)
+         where
+  inducedMap : ⟨ R [ I ]ᵣ ⟩ → ⟨ S ⟩
+  inducedMap = Theory.inducedMap (CommAlgChar.toCommAlg R (S , f)) φ
diff --git a/Cubical/Algebra/CommAlgebra/Instances/Initial.agda b/Cubical/Algebra/CommAlgebra/Instances/Initial.agda
index 26c8b6bdd6..b7babf448d 100644
--- a/Cubical/Algebra/CommAlgebra/Instances/Initial.agda
+++ b/Cubical/Algebra/CommAlgebra/Instances/Initial.agda
@@ -64,8 +64,8 @@ module _ (R : CommRing ℓ) where
                            x * (y * 1a)                   ≡[ i ]⟨ x * (·IdL (y * 1a) (~ i)) ⟩
                            x * (1a · (y * 1a))            ≡⟨ sym (⋆AssocL _ _ _) ⟩
                            (x * 1a) · (y * 1a) ∎)
-        (λ r x → (r · x) * 1a   ≡⟨ ⋆Assoc _ _ _ ⟩
-                         (r * (x * 1a)) ∎)
+        (λ r → (r · _) * 1a   ≡⟨ cong (_* 1a) (·IdR r) ⟩
+               (r * 1a) ∎)
 
     initialMapEq : (f : CommAlgebraHom initialCAlg A)
                    → f ≡ initialMap
diff --git a/Cubical/Algebra/CommAlgebra/Properties.agda b/Cubical/Algebra/CommAlgebra/Properties.agda
index fd75d7d0cd..bd6bb63a90 100644
--- a/Cubical/Algebra/CommAlgebra/Properties.agda
+++ b/Cubical/Algebra/CommAlgebra/Properties.agda
@@ -14,6 +14,8 @@ open import Cubical.Foundations.SIP
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Path
 
+open import Cubical.Functions.Embedding
+
 open import Cubical.Data.Sigma
 
 open import Cubical.Reflection.StrictEquiv
@@ -157,10 +159,11 @@ module CommAlgChar (R : CommRing ℓ) {ℓ' : Level} where
    instance
     _ = snd A
     _ = snd B
-   pres⋆h : ∀ r x → fst h (fst f r · x) ≡ fst g r · fst h x
-   pres⋆h r x = fst h (fst f r · x)       ≡⟨ pres· (snd h) _ _ ⟩
-                fst h (fst f r) · fst h x ≡⟨ cong (λ φ → fst φ r · fst h x) commDiag ⟩
-                fst g r · fst h x ∎
+   pres⋆h : ∀ r → fst h (fst f r · 1r) ≡ fst g r · 1r
+   pres⋆h r = fst h (fst f r · 1r)       ≡⟨ pres· (snd h) _ _ ⟩
+              fst h (fst f r) · fst h 1r ≡⟨ cong (λ φ → fst φ r · fst h 1r) commDiag ⟩
+              fst g r · fst h 1r         ≡⟨ cong (fst g r ·_) (pres1 (snd h))  ⟩
+              fst g r · 1r ∎
 
  fromCommAlgebraHom : (A B : CommAlgebra R ℓ') → CommAlgebraHom A B
                     → CommRingWithHomHom (fromCommAlg A) (fromCommAlg B)
@@ -221,60 +224,37 @@ module CommAlgebraHoms {R : CommRing ℓ} where
   compAssocCommAlgebraHom = compAssocAlgebraHom
 
 module CommAlgebraEquivs {R : CommRing ℓ} where
- open AlgebraEquivs
-
- compCommAlgebraEquiv : {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''} {C : CommAlgebra R ℓ'''}
-                   → CommAlgebraEquiv A B → CommAlgebraEquiv B C → CommAlgebraEquiv A C
- compCommAlgebraEquiv {A = A} {B = B} {C = C} = compAlgebraEquiv {A = CommAlgebra→Algebra A}
-                                                           {B = CommAlgebra→Algebra B}
-                                                           {C = CommAlgebra→Algebra C}
-
+  open AlgebraEquivs
+
+  compCommAlgebraEquiv : {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''} {C : CommAlgebra R ℓ'''}
+                    → CommAlgebraEquiv A B → CommAlgebraEquiv B C → CommAlgebraEquiv A C
+  compCommAlgebraEquiv {A = A} {B = B} {C = C} = compAlgebraEquiv {A = CommAlgebra→Algebra A}
+                                                            {B = CommAlgebra→Algebra B}
+                                                            {C = CommAlgebra→Algebra C}
+
+
+  isSetCommAlgStr : (A : Type ℓ') → isSet (CommAlgebraStr R A)
+  isSetCommAlgStr A =
+    let open CommAlgebraStr
+    in isOfHLevelSucIfInhabited→isOfHLevelSuc 1 (λ str →
+       isOfHLevelRetractFromIso 2 CommAlgebraStrIsoΣ $
+       isSetΣ (str .is-set) λ _ →
+       isSetΣ (str .is-set) (λ _ →
+       isSetΣ (isSet→ (isSet→ (str .is-set))) λ _ →
+       isSetΣ (isSet→ (isSet→ (str .is-set))) (λ _ →
+       isSetΣ (isSet→ (str .is-set)) λ _ →
+       isSetΣSndProp (isSet→ (isSet→ (str .is-set))) (λ _ →
+       isPropIsCommAlgebra R _ _ _ _ _ _))))
 
 -- the CommAlgebra version of uaCompEquiv
 module CommAlgebraUAFunctoriality {R : CommRing ℓ} where
  open CommAlgebraStr
  open CommAlgebraEquivs
 
- CommAlgebra≡ : (A B : CommAlgebra R ℓ') → (
-   Σ[ p ∈ ⟨ A ⟩ ≡ ⟨ B ⟩ ]
-   Σ[ q0 ∈ PathP (λ i → p i) (0a (snd A)) (0a (snd B)) ]
-   Σ[ q1 ∈ PathP (λ i → p i) (1a (snd A)) (1a (snd B)) ]
-   Σ[ r+ ∈ PathP (λ i → p i → p i → p i) (_+_ (snd A)) (_+_ (snd B)) ]
-   Σ[ r· ∈ PathP (λ i → p i → p i → p i) (_·_ (snd A)) (_·_ (snd B)) ]
-   Σ[ s- ∈ PathP (λ i → p i → p i) (-_ (snd A)) (-_ (snd B)) ]
-   Σ[ s⋆ ∈ PathP (λ i → ⟨ R ⟩ → p i → p i) (_⋆_ (snd A)) (_⋆_ (snd B)) ]
-   PathP (λ i → IsCommAlgebra R (q0 i) (q1 i) (r+ i) (r· i) (s- i) (s⋆ i)) (isCommAlgebra (snd A))
-                                                                           (isCommAlgebra (snd B)))
-   ≃ (A ≡ B)
- CommAlgebra≡ A B = isoToEquiv theIso
-   where
-   open Iso
-   theIso : Iso _ _
-   fun theIso (p , q0 , q1 , r+ , r· , s- , s⋆ , t) i = p i
-                 , commalgebrastr (q0 i) (q1 i) (r+ i) (r· i) (s- i) (s⋆ i) (t i)
-   inv theIso x = cong ⟨_⟩ x , cong (0a ∘ snd) x , cong (1a ∘ snd) x
-                , cong (_+_ ∘ snd) x , cong (_·_ ∘ snd) x , cong (-_ ∘ snd) x , cong (_⋆_ ∘ snd) x
-                , cong (isCommAlgebra ∘ snd) x
-   rightInv theIso _ = refl
-   leftInv theIso _ = refl
-
  caracCommAlgebra≡ : {A B : CommAlgebra R ℓ'} (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q
- caracCommAlgebra≡ {A = A} {B = B} p q P =
-   sym (transportTransport⁻ (ua (CommAlgebra≡ A B)) p)
-                                    ∙∙ cong (transport (ua (CommAlgebra≡ A B))) helper
-                                    ∙∙ transportTransport⁻ (ua (CommAlgebra≡ A B)) q
-     where
-     helper : transport (sym (ua (CommAlgebra≡ A B))) p ≡ transport (sym (ua (CommAlgebra≡ A B))) q
-     helper = Σ≡Prop
-                (λ _ → isPropΣ
-                          (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ λ _ → is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
-                          λ _ → isOfHLevelPathP 1 (isPropIsCommAlgebra _ _ _ _ _ _ _) _ _)
-               (transportRefl (cong ⟨_⟩ p) ∙ P ∙ sym (transportRefl (cong ⟨_⟩ q)))
+ caracCommAlgebra≡  _ _ α =
+   isEmbedding→Inj (iso→isEmbedding (invIso ΣPathIsoPathΣ)) _ _ $
+   Σ≡Prop (λ _ → isOfHLevelPathP' 1 (isSetCommAlgStr _) _ _) α
 
  uaCompCommAlgebraEquiv : {A B C : CommAlgebra R ℓ'} (f : CommAlgebraEquiv A B) (g : CommAlgebraEquiv B C)
                   → uaCommAlgebra (compCommAlgebraEquiv f g) ≡ uaCommAlgebra f ∙ uaCommAlgebra g
@@ -285,7 +265,6 @@ module CommAlgebraUAFunctoriality {R : CommRing ℓ} where
      ≡⟨ sym (cong-∙ ⟨_⟩ (uaCommAlgebra f) (uaCommAlgebra g)) ⟩
    cong ⟨_⟩ (uaCommAlgebra f ∙ uaCommAlgebra g) ∎)
 
-
 open CommAlgebraHoms
 open CommAlgebraEquivs
 open CommAlgebraUAFunctoriality
@@ -299,6 +278,7 @@ recPT→CommAlgebra 𝓕 σ compCoh = GpdElim.rec→Gpd isGroupoidCommAlgebra 
                           λ x y z → sym (  cong uaCommAlgebra (compCoh x y z)
                                          ∙ uaCompCommAlgebraEquiv (σ x y) (σ y z)))
 
+open CommAlgebraHoms
 
 contrCommAlgebraHom→contrCommAlgebraEquiv : {R : CommRing ℓ} {A : Type ℓ'}
         (σ : A → CommAlgebra R ℓ'')
diff --git a/Cubical/Algebra/CommAlgebra/Subalgebra.agda b/Cubical/Algebra/CommAlgebra/Subalgebra.agda
index 107a54f296..c4ca6f28ba 100644
--- a/Cubical/Algebra/CommAlgebra/Subalgebra.agda
+++ b/Cubical/Algebra/CommAlgebra/Subalgebra.agda
@@ -20,14 +20,15 @@ module _ (S : Subalgebra) where
   Subalgebra→CommAlgebra≡ = Subalgebra→Algebra≡ S
 
   Subalgebra→CommAlgebra : CommAlgebra R ℓ'
-  Subalgebra→CommAlgebra =
-      Subalgebra→Algebra S .fst
-    , record
-      { AlgebraStr (Subalgebra→Algebra S .snd)
-      ; isCommAlgebra = iscommalgebra
-          (Subalgebra→Algebra S .snd .AlgebraStr.isAlgebra)
-          (λ x y → Subalgebra→CommAlgebra≡
-            (CommAlgebraStr.·Comm (snd A) (fst x) (fst y)))}
+  fst Subalgebra→CommAlgebra = Subalgebra→Algebra S .fst
+  snd Subalgebra→CommAlgebra = record
+                                { AlgebraStr (Subalgebra→Algebra S .snd)
+                                ; isCommAlgebra = record {
+                                    isAlgebra =
+                                       Subalgebra→Algebra S .snd .AlgebraStr.isAlgebra ;
+                                    ·Comm = λ x y → Subalgebra→CommAlgebra≡
+                                       (CommAlgebraStr.·Comm (snd A) (fst x) (fst y)) }
+                                }
 
   Subalgebra→CommAlgebraHom : CommAlgebraHom Subalgebra→CommAlgebra A
   Subalgebra→CommAlgebraHom = Subalgebra→AlgebraHom S
@@ -41,4 +42,3 @@ module _ (S : Subalgebra) where
                               (λ x y → Subalgebra→CommAlgebra≡ (pres+ x y))
                               (λ x y → Subalgebra→CommAlgebra≡ (pres· x y))
                               (λ x y → Subalgebra→CommAlgebra≡ (pres⋆ x y))
-