From e62abab13c1644020e3f0c42f34c57d913f7b60f Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Mon, 30 Sep 2024 18:30:09 +0200 Subject: [PATCH] fix comment --- .../CommRing/Instances/Polynomials/Typevariate/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Base.agda b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Base.agda index 93c792d11..3f06b0e2c 100644 --- a/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Base.agda +++ b/Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Base.agda @@ -15,7 +15,7 @@ module Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.Base where This file contains * the definition of the free commutative algebra on a type I over a commutative ring R as a HIT (let us call that R[I]) - * a prove that the construction is an commutative R-algebra + * the homomorphism R -> R[I], which turns this CommRing into a CommAlgebra For more, see the Properties file. -} open import Cubical.Foundations.Prelude