diff --git a/Cubical/Algebra/CommAlgebra/FP/Instances.agda b/Cubical/Algebra/CommAlgebra/FP/Instances.agda
index 09738084d..6e3a42310 100644
--- a/Cubical/Algebra/CommAlgebra/FP/Instances.agda
+++ b/Cubical/Algebra/CommAlgebra/FP/Instances.agda
@@ -45,6 +45,7 @@ private
 module _ (R : CommRing ℓ) where
   open FinitePresentation
 
+  {- Every (multivariate) polynomial algebra is finitely presented -}
   module _ (n : ℕ) where
     private
       abstract
@@ -52,7 +53,8 @@ module _ (R : CommRing ℓ) where
         p = sym $ 0FGIdeal≡0Ideal (Polynomials R n)
 
       compute :
-        CommAlgebraEquiv (Polynomials R n) $ (Polynomials R n) / ⟨ emptyFinVec ⟨ Polynomials R n ⟩ₐ ⟩[ _ ]
+        CommAlgebraEquiv (Polynomials R n)
+                         ((Polynomials R n) / ⟨ emptyFinVec ⟨ Polynomials R n ⟩ₐ ⟩[ _ ])
       compute =
         transport (λ i → CommAlgebraEquiv (Polynomials R n) ((Polynomials R n) / (p i))) $
           zeroIdealQuotient (Polynomials R n)
@@ -69,54 +71,6 @@ module _ (R : CommRing ℓ) where
 {-
 
 
-  {- Every (multivariate) polynomial algebra is finitely presented -}
-  module _ (n : ℕ) where
-    private
-      A : CommAlgebra R ℓ
-      A = Polynomials n
-
-      emptyGen : FinVec (fst A) 0
-      emptyGen = λ ()
-
-      B : CommAlgebra R ℓ
-      B = FPAlgebra n emptyGen
-
-    polynomialAlgFP : FinitePresentation A
-    FinitePresentation.n polynomialAlgFP = n
-    m polynomialAlgFP = 0
-    relations polynomialAlgFP = emptyGen
-    equiv polynomialAlgFP =
-      -- Idea: A and B enjoy the same universal property.
-      toAAsEquiv , snd toA
-      where
-        toA : CommAlgebraHom B A
-        toA = inducedHom n emptyGen A Construction.var (λ ())
-        fromA : CommAlgebraHom A B
-        fromA = freeInducedHom B (generator _ _)
-        open AlgebraHoms
-        inverse1 : fromA ∘a toA ≡ idAlgebraHom _
-        inverse1 =
-          fromA ∘a toA
-            ≡⟨ sym (unique _ _ B _ _ _ (λ i → cong (fst fromA) (
-                 fst toA (generator n emptyGen i)
-                   ≡⟨ inducedHomOnGenerators _ _ _ _ _ _ ⟩
-                 Construction.var i
-                   ∎))) ⟩
-          inducedHom n emptyGen B (generator _ _) (relationsHold _ _)
-            ≡⟨ unique _ _ B _ _ _ (λ i → refl) ⟩
-          idAlgebraHom _
-            ∎
-        inverse2 : toA ∘a fromA ≡ idAlgebraHom _
-        inverse2 = isoFunInjective (homMapIso A) _ _ (
-          evaluateAt A (toA ∘a fromA)   ≡⟨ sym (naturalEvR {A = B} {B = A} toA fromA) ⟩
-          fst toA ∘ evaluateAt B fromA  ≡⟨ refl ⟩
-          fst toA ∘ generator _ _       ≡⟨ funExt (inducedHomOnGenerators _ _ _ _ _)⟩
-          Construction.var              ∎)
-        toAAsEquiv : ⟨ B ⟩ ≃ ⟨ A ⟩
-        toAAsEquiv = isoToEquiv (iso (fst toA)
-                                     (fst fromA)
-                                     (λ a i → fst (inverse2 i) a)
-                                     (λ b i → fst (inverse1 i) b))
 
   {- The initial R-algebra is finitely presented -}
   private
diff --git a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda
index 3290a2276..7ce31c7d2 100644
--- a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda
+++ b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda
@@ -17,7 +17,8 @@ open import Cubical.Data.Sum as ⊎
 open import Cubical.Data.Sigma
 
 open import Cubical.Algebra.CommRing
-open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate
+open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.Base
+open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.UniversalProperty
 
 private
   variable
diff --git a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda
index 0af77c592..bde4d50ea 100644
--- a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda
+++ b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda
@@ -1,18 +1,12 @@
 {-# OPTIONS --safe #-}
 module Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.Properties where
-{-
-  This file contains
-  * an elimination principle for proving some proposition for all elements of R[I]ᵣ
-    ('elimProp')
-  * definitions of the induced maps appearing in the universal property of R[I],
--}
 
 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.Function
 open import Cubical.Foundations.Isomorphism
 
 open import Cubical.Data.Sigma.Properties using (Σ≡Prop)
@@ -20,9 +14,9 @@ open import Cubical.HITs.SetTruncation
 
 open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.Base
-open import Cubical.Algebra.Ring.Properties
+open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.UniversalProperty public
 
-open import Cubical.Data.Empty
+open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Sigma
 
 open import Cubical.Tactics.CommRingSolver
@@ -31,255 +25,30 @@ private
   variable
     ℓ ℓ' ℓ'' : Level
 
-module _ {R : CommRing ℓ} {I : Type ℓ'} where
+module _ {R : CommRing ℓ} where
   open CommRingStr ⦃...⦄
   private instance
     _ = snd R
-    _ = snd (R [ I ])
 
-  module C = Construction
-  open C using (const)
+  polynomialsOn⊥ : CommRingEquiv (R [ ⊥ ]) R
+  polynomialsOn⊥ =
+    isoToEquiv
+      (iso (to .fst) (from .fst)
+           (λ x → cong (λ f → f .fst x) to∘from)
+           (λ x → cong (λ f → f .fst x) from∘to)) ,
+    isHom
+    where to : CommRingHom (R [ ⊥ ]) R
+          to = inducedHom R (idCommRingHom R) ⊥.rec
 
-  {-
-    Construction of the 'elimProp' eliminator.
-  -}
-  module _
-    {P : ⟨ R [ I ] ⟩ → Type ℓ''}
-    (isPropP : {x : _} → isProp (P x))
-    (onVar : {x : I} → P (C.var x))
-    (onConst : {r : ⟨ R ⟩} → P (const r))
-    (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
+          from : CommRingHom R (R [ ⊥ ])
+          from = constPolynomial R ⊥
 
-    private
-      on- : {x : ⟨ R [ I ] ⟩} → P x → P (- x)
-      on- {x} Px = subst P (minusByMult x) (on· onConst Px)
-        where minusByMult : (x : _) → (const (- 1r)) · x ≡ - x
-              minusByMult x =
-                (const (- 1r)) · x ≡⟨ cong (_· x) (pres- 1r) ⟩
-                (- const (1r)) · x ≡⟨ cong (λ u → (- u) · x) pres1 ⟩
-                (- 1r) · x         ≡⟨ sym (-IsMult-1 x) ⟩
-                - x  ∎
-                where open RingTheory (CommRing→Ring (R [ I ])) using (-IsMult-1)
-                      open IsCommRingHom (constPolynomial R I .snd)
+          to∘from : to ∘cr from ≡ idCommRingHom R
+          to∘from = CommRingHom≡ refl
 
-      -- A helper to deal with the path constructor cases.
-      mkPathP :
-        {x0 x1 : ⟨ R [ I ] ⟩} →
-        (p : x0 ≡ x1) →
-        (Px0 : P (x0)) →
-        (Px1 : P (x1)) →
-        PathP (λ i → P (p i)) Px0 Px1
-      mkPathP _ = isProp→PathP λ i → isPropP
+          from∘to : from ∘cr to ≡ idCommRingHom (R [ ⊥ ])
+          from∘to = idByIdOnVars (from ∘cr to) refl (funExt ⊥.elim)
 
-    elimProp : ((x : _) → P x)
-
-    elimProp (C.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
-
-  {-
-    Construction of the induced map.
-    In this module and the module below, we will show the universal property
-    of the polynomial ring as a commutative ring.
-
-       R ──→ R[I]
-        \     ∣
-         f    ∃!          for a given φ : I → S
-          ↘  ↙
-            S
-
-  -}
-  module _ (S : CommRing ℓ'') (f : CommRingHom R S) (φ : I → ⟨ S ⟩) where
-    private instance
-      _ = S .snd
-
-    open IsCommRingHom
-
-    inducedMap : ⟨ R [ I ] ⟩ → ⟨ S ⟩
-    inducedMap (C.var x) = φ x
-    inducedMap (const r) = (f .fst r)
-    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)) ≡⟨⟩
-             (inducedMap P) + ((f .fst 0r))           ≡⟨ cong ((inducedMap P) +_) (pres0 (f .snd)) ⟩
-             (inducedMap P) + 0r                      ≡⟨ +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 _ ⟩
-               0r                            ≡⟨ sym (pres0 (f .snd)) ⟩
-               (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) (pres1 (f .snd)) ⟩
-               1r · 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) = pres+ (f .snd) s t i
-    inducedMap (C.·HomConst s t i) = pres· (f .snd) s t 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 IsCommRingHom
-
-      inducedHom : CommRingHom (R [ I ]) S
-      inducedHom .fst = inducedMap
-      inducedHom .snd .pres0 = pres0 (f .snd)
-      inducedHom .snd .pres1 = pres1 (f. snd)
-      inducedHom .snd .pres+ = λ _ _ → refl
-      inducedHom .snd .pres· = λ _ _ → refl
-      inducedHom .snd .pres- = λ _ → refl
-
-    opaque
-      inducedHomComm : inducedHom ∘cr constPolynomial R I ≡ f
-      inducedHomComm = CommRingHom≡ $ funExt (λ r → refl)
-
-module _  {R : CommRing ℓ} {I : Type ℓ'} (S : CommRing ℓ'') (f : CommRingHom R S) where
-  open CommRingStr ⦃...⦄
-  private instance
-    _ = S .snd
-    _ = (R [ I ]) .snd
-  open IsCommRingHom
-
-  evalVar : CommRingHom (R [ I ]) S → I → ⟨ S ⟩
-  evalVar h = h .fst ∘ var
-
-  opaque
-    unfolding var
-    evalInduce : ∀ (φ : I → ⟨ S ⟩)
-                 → evalVar (inducedHom S f φ) ≡ φ
-    evalInduce φ = refl
-
-  opaque
-    unfolding var
-    evalOnVars : ∀ (φ : I → ⟨ S ⟩)
-                 → (i : I) → inducedHom S f φ .fst (var i) ≡ φ i
-    evalOnVars φ i = refl
-
-  opaque
-    unfolding var
-    induceEval : (g : CommRingHom (R [ I ]) S)
-                 (p : g .fst ∘ constPolynomial R I .fst ≡ f .fst)
-                 → (inducedHom S f (evalVar g)) ≡ g
-    induceEval g p =
-      let theMap : ⟨ R [ I ] ⟩ → ⟨ S ⟩
-          theMap = inducedMap S f (evalVar g)
-      in
-      CommRingHom≡ $
-      funExt $
-      elimProp
-        (is-set _ _)
-        (λ {x} → refl)
-        (λ {r} →  sym (cong (λ f → f r) p))
-        (λ {x} {y} eq-x eq-y →
-          theMap (x + y)        ≡⟨ pres+ (inducedHom S f (evalVar g) .snd) x y ⟩
-          theMap x + theMap y   ≡[ i ]⟨ (eq-x i + eq-y i) ⟩
-          (g $cr x + g $cr y)   ≡⟨ sym (pres+ (g .snd) _ _) ⟩
-          (g $cr (x + y)) ∎)
-        λ {x} {y} eq-x eq-y →
-          theMap (x · y)        ≡⟨ pres· (inducedHom S f (evalVar g) .snd) x y ⟩
-          theMap x · theMap y   ≡[ i ]⟨ (eq-x i · eq-y i) ⟩
-          (g $cr x · g $cr y)   ≡⟨ sym (pres· (g .snd) _ _) ⟩
-          (g $cr (x · y)) ∎
-
-  opaque
-    inducedHomUnique : (φ : I → ⟨ S ⟩)
-                 (g : CommRingHom (R [ I ]) S)
-                 (p : g .fst ∘ constPolynomial R I .fst ≡ f .fst)
-                 (q : evalVar g ≡ φ)
-                 → inducedHom S f φ ≡ g
-    inducedHomUnique φ g p q = cong (inducedHom S f) (sym q) ∙ induceEval g p
-
-  opaque
-    hom≡ByValuesOnVars : (g h : CommRingHom (R [ I ]) S)
-                         (p : g .fst ∘ constPolynomial _ _ .fst ≡ f .fst) (q : h .fst ∘ constPolynomial _ _ .fst ≡ f .fst)
-                         → (evalVar g ≡ evalVar h)
-                         → g ≡ h
-    hom≡ByValuesOnVars g h p q ≡OnVars =
-      sym (inducedHomUnique ϕ g p refl) ∙ inducedHomUnique ϕ h q (sym ≡OnVars)
-      where ϕ : I → ⟨ S ⟩
-            ϕ = evalVar g
-
-opaque
-  idByIdOnVars : {R : CommRing ℓ} {I : Type ℓ'}
-                 (g : CommRingHom (R [ I ]) (R [ I ]))
-                 (p : g .fst ∘ constPolynomial _ _ .fst ≡ constPolynomial _ _ .fst)
-                 → (g .fst ∘ var ≡ idfun _ ∘ var)
-                 → g ≡ idCommRingHom (R [ I ])
-  idByIdOnVars g p idOnVars = hom≡ByValuesOnVars _ (constPolynomial _ _) g (idCommRingHom _) p refl idOnVars
+          abstract
+            isHom : IsCommRingHom ((R [ ⊥ ]) .snd) (to .fst) (R .snd)
+            isHom = to .snd
diff --git a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/UniversalProperty.agda b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/UniversalProperty.agda
new file mode 100644
index 000000000..50e6aaf81
--- /dev/null
+++ b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/UniversalProperty.agda
@@ -0,0 +1,285 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.UniversalProperty where
+{-
+  This file contains
+  * an elimination principle for proving some proposition for all elements of R[I]ᵣ
+    ('elimProp')
+  * definitions of the induced maps appearing in the universal property of R[I],
+-}
+
+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.CommRing.Instances.Polynomials.Typevariate.Base
+open import Cubical.Algebra.Ring.Properties
+
+open import Cubical.Data.Empty
+open import Cubical.Data.Sigma
+
+open import Cubical.Tactics.CommRingSolver
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+module _ {R : CommRing ℓ} {I : Type ℓ'} where
+  open CommRingStr ⦃...⦄
+  private instance
+    _ = snd R
+    _ = snd (R [ I ])
+
+  module C = Construction
+  open C using (const)
+
+  {-
+    Construction of the 'elimProp' eliminator.
+  -}
+  module _
+    {P : ⟨ R [ I ] ⟩ → Type ℓ''}
+    (isPropP : {x : _} → isProp (P x))
+    (onVar : {x : I} → P (C.var x))
+    (onConst : {r : ⟨ R ⟩} → P (const r))
+    (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 (- x)
+      on- {x} Px = subst P (minusByMult x) (on· onConst Px)
+        where minusByMult : (x : _) → (const (- 1r)) · x ≡ - x
+              minusByMult x =
+                (const (- 1r)) · x ≡⟨ cong (_· x) (pres- 1r) ⟩
+                (- const (1r)) · x ≡⟨ cong (λ u → (- u) · x) pres1 ⟩
+                (- 1r) · x         ≡⟨ sym (-IsMult-1 x) ⟩
+                - x  ∎
+                where open RingTheory (CommRing→Ring (R [ I ])) using (-IsMult-1)
+                      open IsCommRingHom (constPolynomial R I .snd)
+
+      -- A helper to deal with the path constructor cases.
+      mkPathP :
+        {x0 x1 : ⟨ R [ I ] ⟩} →
+        (p : x0 ≡ x1) →
+        (Px0 : P (x0)) →
+        (Px1 : P (x1)) →
+        PathP (λ i → P (p i)) Px0 Px1
+      mkPathP _ = isProp→PathP λ i → isPropP
+
+    elimProp : ((x : _) → P x)
+
+    elimProp (C.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
+
+  {-
+    Construction of the induced map.
+    In this module and the module below, we will show the universal property
+    of the polynomial ring as a commutative ring.
+
+       R ──→ R[I]
+        \     ∣
+         f    ∃!          for a given φ : I → S
+          ↘  ↙
+            S
+
+  -}
+  module _ (S : CommRing ℓ'') (f : CommRingHom R S) (φ : I → ⟨ S ⟩) where
+    private instance
+      _ = S .snd
+
+    open IsCommRingHom
+
+    inducedMap : ⟨ R [ I ] ⟩ → ⟨ S ⟩
+    inducedMap (C.var x) = φ x
+    inducedMap (const r) = (f .fst r)
+    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)) ≡⟨⟩
+             (inducedMap P) + ((f .fst 0r))           ≡⟨ cong ((inducedMap P) +_) (pres0 (f .snd)) ⟩
+             (inducedMap P) + 0r                      ≡⟨ +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 _ ⟩
+               0r                            ≡⟨ sym (pres0 (f .snd)) ⟩
+               (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) (pres1 (f .snd)) ⟩
+               1r · 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) = pres+ (f .snd) s t i
+    inducedMap (C.·HomConst s t i) = pres· (f .snd) s t 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 IsCommRingHom
+
+      inducedHom : CommRingHom (R [ I ]) S
+      inducedHom .fst = inducedMap
+      inducedHom .snd .pres0 = pres0 (f .snd)
+      inducedHom .snd .pres1 = pres1 (f. snd)
+      inducedHom .snd .pres+ = λ _ _ → refl
+      inducedHom .snd .pres· = λ _ _ → refl
+      inducedHom .snd .pres- = λ _ → refl
+
+    opaque
+      inducedHomComm : inducedHom ∘cr constPolynomial R I ≡ f
+      inducedHomComm = CommRingHom≡ $ funExt (λ r → refl)
+
+module _  {R : CommRing ℓ} {I : Type ℓ'} (S : CommRing ℓ'') (f : CommRingHom R S) where
+  open CommRingStr ⦃...⦄
+  private instance
+    _ = S .snd
+    _ = (R [ I ]) .snd
+  open IsCommRingHom
+
+  evalVar : CommRingHom (R [ I ]) S → I → ⟨ S ⟩
+  evalVar h = h .fst ∘ var
+
+  opaque
+    unfolding var
+    evalInduce : ∀ (φ : I → ⟨ S ⟩)
+                 → evalVar (inducedHom S f φ) ≡ φ
+    evalInduce φ = refl
+
+  opaque
+    unfolding var
+    evalOnVars : ∀ (φ : I → ⟨ S ⟩)
+                 → (i : I) → inducedHom S f φ .fst (var i) ≡ φ i
+    evalOnVars φ i = refl
+
+  opaque
+    unfolding var
+    induceEval : (g : CommRingHom (R [ I ]) S)
+                 (p : g .fst ∘ constPolynomial R I .fst ≡ f .fst)
+                 → (inducedHom S f (evalVar g)) ≡ g
+    induceEval g p =
+      let theMap : ⟨ R [ I ] ⟩ → ⟨ S ⟩
+          theMap = inducedMap S f (evalVar g)
+      in
+      CommRingHom≡ $
+      funExt $
+      elimProp
+        (is-set _ _)
+        (λ {x} → refl)
+        (λ {r} →  sym (cong (λ f → f r) p))
+        (λ {x} {y} eq-x eq-y →
+          theMap (x + y)        ≡⟨ pres+ (inducedHom S f (evalVar g) .snd) x y ⟩
+          theMap x + theMap y   ≡[ i ]⟨ (eq-x i + eq-y i) ⟩
+          (g $cr x + g $cr y)   ≡⟨ sym (pres+ (g .snd) _ _) ⟩
+          (g $cr (x + y)) ∎)
+        λ {x} {y} eq-x eq-y →
+          theMap (x · y)        ≡⟨ pres· (inducedHom S f (evalVar g) .snd) x y ⟩
+          theMap x · theMap y   ≡[ i ]⟨ (eq-x i · eq-y i) ⟩
+          (g $cr x · g $cr y)   ≡⟨ sym (pres· (g .snd) _ _) ⟩
+          (g $cr (x · y)) ∎
+
+  opaque
+    inducedHomUnique : (φ : I → ⟨ S ⟩)
+                 (g : CommRingHom (R [ I ]) S)
+                 (p : g .fst ∘ constPolynomial R I .fst ≡ f .fst)
+                 (q : evalVar g ≡ φ)
+                 → inducedHom S f φ ≡ g
+    inducedHomUnique φ g p q = cong (inducedHom S f) (sym q) ∙ induceEval g p
+
+  opaque
+    hom≡ByValuesOnVars : (g h : CommRingHom (R [ I ]) S)
+                         (p : g .fst ∘ constPolynomial _ _ .fst ≡ f .fst) (q : h .fst ∘ constPolynomial _ _ .fst ≡ f .fst)
+                         → (evalVar g ≡ evalVar h)
+                         → g ≡ h
+    hom≡ByValuesOnVars g h p q ≡OnVars =
+      sym (inducedHomUnique ϕ g p refl) ∙ inducedHomUnique ϕ h q (sym ≡OnVars)
+      where ϕ : I → ⟨ S ⟩
+            ϕ = evalVar g
+
+opaque
+  idByIdOnVars : {R : CommRing ℓ} {I : Type ℓ'}
+                 (g : CommRingHom (R [ I ]) (R [ I ]))
+                 (p : g .fst ∘ constPolynomial _ _ .fst ≡ constPolynomial _ _ .fst)
+                 → (g .fst ∘ var ≡ idfun _ ∘ var)
+                 → g ≡ idCommRingHom (R [ I ])
+  idByIdOnVars g p idOnVars = hom≡ByValuesOnVars _ (constPolynomial _ _) g (idCommRingHom _) p refl idOnVars