From 901cfa97083407a724eb574887908e7a04735b6b Mon Sep 17 00:00:00 2001 From: felixwellen Date: Thu, 24 Aug 2023 21:03:42 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20agda/cub?= =?UTF-8?q?ical@bec2e9c402b66b86a1f2ef15a9fc32595e7ecf1d=20=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...al.Algebra.CommAlgebra.FPAlgebra.Base.html | 40 +- ...gebra.CommAlgebra.FPAlgebra.Instances.html | 16 +- ...ebra.CommAlgebra.FreeCommAlgebra.Base.html | 163 ++-- ...mmAlgebra.FreeCommAlgebra.OnCoproduct.html | 164 ++-- ...ommAlgebra.FreeCommAlgebra.Properties.html | 892 +++++++++--------- ...ypevariateHIT.EquivUnivariateListPoly.html | 24 +- 6 files changed, 652 insertions(+), 647 deletions(-) diff --git a/Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html b/Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html index 23e904bba8..6a0e8434bc 100644 --- a/Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html +++ b/Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html @@ -21,7 +21,7 @@ open import Cubical.Algebra.CommRing.FGIdeal using (inclOfFGIdeal) open import Cubical.Algebra.CommAlgebra open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra - renaming (inducedHom to freeInducedHom) + renaming (inducedHom to freeInducedHom) open import Cubical.Algebra.CommAlgebra.QuotientAlgebra renaming (inducedHom to quotientInducedHom) open import Cubical.Algebra.CommAlgebra.Ideal @@ -36,15 +36,15 @@ ℓ ℓ' : Level module _ {R : CommRing ℓ} where - open Construction using (var) + open Construction using (var) Polynomials : (n : ℕ) → CommAlgebra R ℓ - Polynomials n = R [ Fin n ] + Polynomials n = R [ Fin n ] evPoly : {n : ℕ} (A : CommAlgebra R ℓ) → ⟨ Polynomials n ⟩ → FinVec ⟨ A ⟩ n → ⟨ A ⟩ evPoly A P values = fst (freeInducedHom A values) P - evPolyPoly : {n : ℕ} (P : ⟨ Polynomials n ⟩) → evPoly (Polynomials n) P var ≡ P - evPolyPoly {n = n} P = cong (λ u → fst u P) (inducedHomVar R (Fin n)) + evPolyPoly : {n : ℕ} (P : ⟨ Polynomials n ⟩) → evPoly (Polynomials n) P var ≡ P + evPolyPoly {n = n} P = cong (λ u → fst u P) (inducedHomVar R (Fin n)) evPolyHomomorphic : {n : ℕ} (A B : CommAlgebra R ℓ) (f : CommAlgebraHom A B) → (P : ⟨ Polynomials n ⟩) → (values : FinVec ⟨ A ⟩ n) @@ -52,7 +52,7 @@ 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 f values) ⟩ fst (freeInducedHom B (fst f ∘ values)) P ≡⟨ refl ⟩ evPoly B P (fst f ∘ values) ∎ where open AlgebraHoms @@ -76,13 +76,13 @@ modRelations = quotientHom (Polynomials n) relationsIdeal generator : (i : Fin n) → ⟨ FPAlgebra ⟩ - generator = fst modRelations ∘ var + generator = fst modRelations ∘ var relationsHold : (i : Fin m) → evPoly FPAlgebra (relation i) generator ≡ 0a (snd FPAlgebra) relationsHold i = evPoly FPAlgebra (relation i) generator - ≡⟨ sym (evPolyHomomorphic (Polynomials n) FPAlgebra modRelations (relation i) var) ⟩ - fst modRelations (evPoly (Polynomials n) (relation i) var) + ≡⟨ sym (evPolyHomomorphic (Polynomials n) FPAlgebra modRelations (relation i) var) ⟩ + fst modRelations (evPoly (Polynomials n) (relation i) var) ≡⟨ cong (λ u → fst modRelations u) (evPolyPoly (relation i)) ⟩ fst modRelations (relation i) ≡⟨ isZeroFromIdeal {R = R} @@ -128,7 +128,7 @@ (i : Fin n) → fst inducedHom (generator i) ≡ values i inducedHomOnGenerators i = - cong (λ f → fst f (var i)) + cong (λ f → fst f (var i)) (inducedHom∘quotientHom (Polynomials n) relationsIdeal A freeHom isInKernel) unique : @@ -144,11 +144,11 @@ f (sym ( f' ≡⟨ sym (inv f') ⟩ - freeInducedHom A (evaluateAt A f') ≡⟨ cong (freeInducedHom A) + freeInducedHom A (evaluateAt A f') ≡⟨ cong (freeInducedHom A) (funExt hasCorrectValues) ⟩ freeInducedHom A values ≡⟨ cong (freeInducedHom A) (sym (funExt inducedHomOnGenerators)) ⟩ - freeInducedHom A (evaluateAt A iHom') ≡⟨ inv iHom' ⟩ + freeInducedHom A (evaluateAt A iHom') ≡⟨ inv iHom' ⟩ iHom' ∎)) where {- @@ -162,8 +162,8 @@ f' = compAlgebraHom modRelations f iHom' = compAlgebraHom modRelations inducedHom - inv : retract (Iso.fun (homMapIso {I = Fin n} A)) (Iso.inv (homMapIso A)) - inv = Iso.leftInv (homMapIso {R = R} {I = Fin n} A) + inv : retract (Iso.fun (homMapIso {I = Fin n} A)) (Iso.inv (homMapIso A)) + inv = Iso.leftInv (homMapIso {R = R} {I = Fin n} A) universal : isContr (Σ[ f ∈ CommAlgebraHom FPAlgebra A ] ((i : Fin n) → fst f (generator i) ≡ values i)) @@ -189,15 +189,15 @@ CommAlgebraHom FPAlgebra A → zeroLocus A evaluateAtFP {A} f = value , λ i → evPoly A (relation i) value ≡⟨ step1 (relation i) ⟩ - fst compHom (evPoly (Polynomials n) (relation i) var) ≡⟨ refl ⟩ + fst compHom (evPoly (Polynomials n) (relation i) var) ≡⟨ refl ⟩ (fst f) ((fst modRelations) - (evPoly (Polynomials n) (relation i) var)) ≡⟨ cong + (evPoly (Polynomials n) (relation i) var)) ≡⟨ cong (fst f) (evPolyHomomorphic (Polynomials n) FPAlgebra modRelations - (relation i) var) ⟩ + (relation i) var) ⟩ (fst f) (evPoly FPAlgebra (relation i) generator) ≡⟨ cong (fst f) (relationsHold i) ⟩ (fst f) (0a (snd FPAlgebra)) ≡⟨ IsAlgebraHom.pres0 (snd f) ⟩ 0a (snd A) ∎ @@ -205,9 +205,9 @@ compHom : CommAlgebraHom (Polynomials n) A compHom = CommAlgebraHoms.compCommAlgebraHom (Polynomials n) FPAlgebra A modRelations f value : FinVec ⟨ A ⟩ n - value = (Iso.fun (homMapIso A)) compHom - step1 : (x : ⟨ Polynomials n ⟩) → evPoly A x value ≡ fst compHom (evPoly (Polynomials n) x var) - step1 x = sym (evPolyHomomorphic (Polynomials n) A compHom x var) + value = (Iso.fun (homMapIso A)) compHom + step1 : (x : ⟨ Polynomials n ⟩) → evPoly A x value ≡ fst compHom (evPoly (Polynomials n) x var) + step1 x = sym (evPolyHomomorphic (Polynomials n) A compHom x var) FPHomIso : {A : CommAlgebra R ℓ} → Iso (CommAlgebraHom FPAlgebra A) (zeroLocus A) diff --git a/Cubical.Algebra.CommAlgebra.FPAlgebra.Instances.html b/Cubical.Algebra.CommAlgebra.FPAlgebra.Instances.html index 95f42e7a9e..17b4f56774 100644 --- a/Cubical.Algebra.CommAlgebra.FPAlgebra.Instances.html +++ b/Cubical.Algebra.CommAlgebra.FPAlgebra.Instances.html @@ -30,7 +30,7 @@ open import Cubical.Algebra.CommRing.FGIdeal using (inclOfFGIdeal) open import Cubical.Algebra.CommAlgebra open import Cubical.Algebra.CommAlgebra.FreeCommAlgebra - renaming (inducedHom to freeInducedHom) + renaming (inducedHom to freeInducedHom) open import Cubical.Algebra.CommAlgebra.QuotientAlgebra renaming (inducedHom to quotientInducedHom) open import Cubical.Algebra.CommAlgebra.Ideal using (IdealsIn) @@ -72,7 +72,7 @@ toAAsEquiv , snd toA where toA : CommAlgebraHom B A - toA = inducedHom n emptyGen A Construction.var (λ ()) + toA = inducedHom n emptyGen A Construction.var (λ ()) fromA : CommAlgebraHom A B fromA = freeInducedHom B (generator _ _) open AlgebraHoms @@ -82,18 +82,18 @@ ≡⟨ sym (unique _ _ _ _ _ _ (λ i → cong (fst fromA) ( fst toA (generator n emptyGen i) ≡⟨ inducedHomOnGenerators _ _ _ _ _ _ ⟩ - Construction.var i + Construction.var i ∎))) ⟩ inducedHom n emptyGen B (generator _ _) (relationsHold _ _) ≡⟨ unique _ _ _ _ _ _ (λ 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 ⟩ + 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 ∎) + Construction.var ∎) toAAsEquiv : ⟨ B ⟩ ≃ ⟨ A ⟩ toAAsEquiv = isoToEquiv (iso (fst toA) (fst fromA) @@ -157,7 +157,7 @@ open CommAlgebraStr ⦃...⦄ private rels : FinVec ⟨ Polynomials {R = R} 0 ⟩ m - rels = Construction.const ∘ xs + rels = Construction.const ∘ xs B = FPAlgebra 0 rels diff --git a/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html b/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html index bdf9a1fcb9..7e1506eae9 100644 --- a/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html +++ b/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html @@ -17,91 +17,82 @@ * 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 - * definitions of the induced maps appearing in the universal property of R[I], - that is: * for any map I → A, where A is a commutative R-algebra, - the induced algebra homomorphism R[I] → A - ('inducedHom') - * for any hom R[I] → A, the 'restricttion to variables' I → A - ('evaluateAt') - * a proof that the two constructions are inverse to each other - ('homRetrievable' and 'mapRetrievable') - * a proof, that the corresponding pointwise equivalence of functors is natural - ('naturalR', 'naturalL') + For more, see the Properties file. -} -open import Cubical.Foundations.Prelude - -open import Cubical.Algebra.CommRing -open import Cubical.Algebra.CommAlgebra.Base - -private - variable - ℓ ℓ' : Level - -module Construction (R : CommRing ℓ) where - open CommRingStr (snd R) using (1r; 0r) renaming (_+_ to _+r_; _·_ to _·r_) - - data R[_] (I : Type ℓ') : Type (ℓ-max ℓ ℓ') where - var : I → R[ I ] - const : fst R → R[ I ] - _+_ : R[ I ] → R[ I ] → R[ I ] - -_ : R[ I ] → R[ I ] - _·_ : R[ I ] → R[ I ] → R[ I ] -- \cdot - - +-assoc : (x y z : R[ I ]) → x + (y + z) ≡ (x + y) + z - +-rid : (x : R[ I ]) → x + (const 0r) ≡ x - +-rinv : (x : R[ I ]) → x + (- x) ≡ (const 0r) - +-comm : (x y : R[ I ]) → x + y ≡ y + x - - ·-assoc : (x y z : R[ I ]) → x · (y · z) ≡ (x · y) · z - ·-lid : (x : R[ I ]) → (const 1r) · x ≡ x - ·-comm : (x y : R[ I ]) → x · y ≡ y · x - - ldist : (x y z : R[ I ]) → (x + y) · z ≡ (x · z) + (y · z) - - +HomConst : (s t : fst R) → const (s +r t) ≡ const s + const t - ·HomConst : (s t : fst R) → const (s ·r t) ≡ (const s) · (const t) - - 0-trunc : (x y : R[ I ]) (p q : x ≡ y) → p ≡ q - - _⋆_ : {I : Type ℓ'} → fst R → R[ I ] → R[ I ] - r ⋆ x = const r · x - - ⋆-assoc : {I : Type ℓ'} → (s t : fst R) (x : R[ I ]) → (s ·r t) ⋆ x ≡ s ⋆ (t ⋆ x) - ⋆-assoc s t x = const (s ·r t) · x ≡⟨ cong (λ u → u · x) (·HomConst _ _) ⟩ - (const s · const t) · x ≡⟨ sym (·-assoc _ _ _) ⟩ - const s · (const t · x) ≡⟨ refl ⟩ - s ⋆ (t ⋆ x) ∎ - - ⋆-ldist-+ : {I : Type ℓ'} → (s t : fst R) (x : R[ I ]) → (s +r t) ⋆ x ≡ (s ⋆ x) + (t ⋆ x) - ⋆-ldist-+ s t x = (s +r t) ⋆ x ≡⟨ cong (λ u → u · x) (+HomConst _ _) ⟩ - (const s + const t) · x ≡⟨ ldist _ _ _ ⟩ - (s ⋆ x) + (t ⋆ x) ∎ - - ⋆-rdist-+ : {I : Type ℓ'} → (s : fst R) (x y : R[ I ]) → s ⋆ (x + y) ≡ (s ⋆ x) + (s ⋆ y) - ⋆-rdist-+ s x y = const s · (x + y) ≡⟨ ·-comm _ _ ⟩ - (x + y) · const s ≡⟨ ldist _ _ _ ⟩ - (x · const s) + (y · const s) ≡⟨ cong (λ u → u + (y · const s)) (·-comm _ _) ⟩ - (s ⋆ x) + (y · const s) ≡⟨ cong (λ u → (s ⋆ x) + u) (·-comm _ _) ⟩ - (s ⋆ x) + (s ⋆ y) ∎ - - ⋆-assoc-· : {I : Type ℓ'} → (s : fst R) (x y : R[ I ]) → (s ⋆ x) · y ≡ s ⋆ (x · y) - ⋆-assoc-· s x y = (s ⋆ x) · y ≡⟨ sym (·-assoc _ _ _) ⟩ - s ⋆ (x · y) ∎ - - 0a : {I : Type ℓ'} → R[ I ] - 0a = (const 0r) - - 1a : {I : Type ℓ'} → R[ I ] - 1a = (const 1r) - - isCommAlgebra : {I : Type ℓ'} → IsCommAlgebra R {A = R[ I ]} 0a 1a _+_ _·_ -_ _⋆_ - isCommAlgebra = makeIsCommAlgebra 0-trunc - +-assoc +-rid +-rinv +-comm - ·-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 - open Construction R +open import Cubical.Foundations.Prelude + +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommAlgebra.Base + +private + variable + ℓ ℓ' : Level + +module Construction (R : CommRing ℓ) where + open CommRingStr (snd R) using (1r; 0r) renaming (_+_ to _+r_; _·_ to _·r_) + + data R[_] (I : Type ℓ') : Type (ℓ-max ℓ ℓ') where + var : I → R[ I ] + const : fst R → R[ I ] + _+_ : R[ I ] → R[ I ] → R[ I ] + -_ : R[ I ] → R[ I ] + _·_ : R[ I ] → R[ I ] → R[ I ] -- \cdot + + +-assoc : (x y z : R[ I ]) → x + (y + z) ≡ (x + y) + z + +-rid : (x : R[ I ]) → x + (const 0r) ≡ x + +-rinv : (x : R[ I ]) → x + (- x) ≡ (const 0r) + +-comm : (x y : R[ I ]) → x + y ≡ y + x + + ·-assoc : (x y z : R[ I ]) → x · (y · z) ≡ (x · y) · z + ·-lid : (x : R[ I ]) → (const 1r) · x ≡ x + ·-comm : (x y : R[ I ]) → x · y ≡ y · x + + ldist : (x y z : R[ I ]) → (x + y) · z ≡ (x · z) + (y · z) + + +HomConst : (s t : fst R) → const (s +r t) ≡ const s + const t + ·HomConst : (s t : fst R) → const (s ·r t) ≡ (const s) · (const t) + + 0-trunc : (x y : R[ I ]) (p q : x ≡ y) → p ≡ q + + _⋆_ : {I : Type ℓ'} → fst R → R[ I ] → R[ I ] + r ⋆ x = const r · x + + ⋆-assoc : {I : Type ℓ'} → (s t : fst R) (x : R[ I ]) → (s ·r t) ⋆ x ≡ s ⋆ (t ⋆ x) + ⋆-assoc s t x = const (s ·r t) · x ≡⟨ cong (λ u → u · x) (·HomConst _ _) ⟩ + (const s · const t) · x ≡⟨ sym (·-assoc _ _ _) ⟩ + const s · (const t · x) ≡⟨ refl ⟩ + s ⋆ (t ⋆ x) ∎ + + ⋆-ldist-+ : {I : Type ℓ'} → (s t : fst R) (x : R[ I ]) → (s +r t) ⋆ x ≡ (s ⋆ x) + (t ⋆ x) + ⋆-ldist-+ s t x = (s +r t) ⋆ x ≡⟨ cong (λ u → u · x) (+HomConst _ _) ⟩ + (const s + const t) · x ≡⟨ ldist _ _ _ ⟩ + (s ⋆ x) + (t ⋆ x) ∎ + + ⋆-rdist-+ : {I : Type ℓ'} → (s : fst R) (x y : R[ I ]) → s ⋆ (x + y) ≡ (s ⋆ x) + (s ⋆ y) + ⋆-rdist-+ s x y = const s · (x + y) ≡⟨ ·-comm _ _ ⟩ + (x + y) · const s ≡⟨ ldist _ _ _ ⟩ + (x · const s) + (y · const s) ≡⟨ cong (λ u → u + (y · const s)) (·-comm _ _) ⟩ + (s ⋆ x) + (y · const s) ≡⟨ cong (λ u → (s ⋆ x) + u) (·-comm _ _) ⟩ + (s ⋆ x) + (s ⋆ y) ∎ + + ⋆-assoc-· : {I : Type ℓ'} → (s : fst R) (x y : R[ I ]) → (s ⋆ x) · y ≡ s ⋆ (x · y) + ⋆-assoc-· s x y = (s ⋆ x) · y ≡⟨ sym (·-assoc _ _ _) ⟩ + s ⋆ (x · y) ∎ + + 0a : {I : Type ℓ'} → R[ I ] + 0a = (const 0r) + + 1a : {I : Type ℓ'} → R[ I ] + 1a = (const 1r) + + isCommAlgebra : {I : Type ℓ'} → IsCommAlgebra R {A = R[ I ]} 0a 1a _+_ _·_ -_ _⋆_ + isCommAlgebra = makeIsCommAlgebra 0-trunc + +-assoc +-rid +-rinv +-comm + ·-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 + open Construction R \ No newline at end of file diff --git a/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.OnCoproduct.html b/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.OnCoproduct.html index b30a1ff60d..64efbe9b17 100644 --- a/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.OnCoproduct.html +++ b/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.OnCoproduct.html @@ -31,28 +31,28 @@ ℓ ℓ' : Level module CalculateFreeCommAlgebraOnCoproduct (R : CommRing ℓ) (I J : Type ℓ) where - open Construction using (var; const) + open Construction using (var; const) open CommAlgebraStr ⦃...⦄ {- We start by defining R[I][J] and R[I⊎J] as R[I] algebras, which we need later to use universal properties -} - R[I][J]overR[I] : CommAlgebra (CommAlgebra→CommRing (R [ I ])) ℓ - R[I][J]overR[I] = (CommAlgebra→CommRing (R [ I ])) [ J ] + R[I][J]overR[I] : CommAlgebra (CommAlgebra→CommRing (R [ I ])) ℓ + R[I][J]overR[I] = (CommAlgebra→CommRing (R [ I ])) [ J ] R[I][J] : CommAlgebra R ℓ - R[I][J] = baseChange baseRingHom R[I][J]overR[I] + R[I][J] = baseChange baseRingHom R[I][J]overR[I] - ψOverR : CommAlgebraHom (R [ I ]) (R [ I ⊎ J ]) - ψOverR = inducedHom (R [ I ⊎ J ]) (λ i → var (inl i)) + ψOverR : CommAlgebraHom (R [ I ]) (R [ I ⊎ J ]) + ψOverR = inducedHom (R [ I ⊎ J ]) (λ i → var (inl i)) - ψ : CommRingHom (CommAlgebra→CommRing (R [ I ])) (CommAlgebra→CommRing (R [ I ⊎ J ])) - ψ = CommAlgebraHom→CommRingHom (R [ I ]) (R [ I ⊎ J ]) ψOverR + ψ : CommRingHom (CommAlgebra→CommRing (R [ I ])) (CommAlgebra→CommRing (R [ I ⊎ J ])) + ψ = CommAlgebraHom→CommRingHom (R [ I ]) (R [ I ⊎ J ]) ψOverR - R[I⊎J]overR[I] : CommAlgebra (CommAlgebra→CommRing (R [ I ])) ℓ - R[I⊎J]overR[I] = Iso.inv (CommAlgChar.CommAlgIso (CommAlgebra→CommRing (R [ I ]))) - (CommAlgebra→CommRing (R [ I ⊎ J ]) , + R[I⊎J]overR[I] : CommAlgebra (CommAlgebra→CommRing (R [ I ])) ℓ + R[I⊎J]overR[I] = Iso.inv (CommAlgChar.CommAlgIso (CommAlgebra→CommRing (R [ I ]))) + (CommAlgebra→CommRing (R [ I ⊎ J ]) , ψ) {- @@ -60,47 +60,47 @@ -} open RingHoms open RingStr ⦃...⦄ using (1r) - instance _ = snd (R [ I ]) + instance _ = snd (R [ I ]) _ = snd R[I⊎J]overR[I] _ = snd (CommRing→Ring R) - module R[I] = CommAlgebraStr (snd (R [ I ])) + module R[I] = CommAlgebraStr (snd (R [ I ])) module R[I⊎J]overR[I] = CommAlgebraStr (snd R[I⊎J]overR[I]) - module R[I⊎J] = CommAlgebraStr (snd (R [ I ⊎ J ])) + module R[I⊎J] = CommAlgebraStr (snd (R [ I ⊎ J ])) - to : CommAlgebraHom (R [ I ⊎ J ]) R[I][J] - to = inducedHom R[I][J] - (⊎.rec (λ i → const (var i)) - λ j → var j) + to : CommAlgebraHom (R [ I ⊎ J ]) R[I][J] + to = inducedHom R[I][J] + (⊎.rec (λ i → const (var i)) + λ j → var j) isoR = CommAlgChar.CommAlgIso R - isoR[I] = CommAlgChar.CommAlgIso (CommAlgebra→CommRing (R [ I ])) + isoR[I] = CommAlgChar.CommAlgIso (CommAlgebra→CommRing (R [ I ])) asHomOverR[I] = Iso.fun isoR[I] R[I⊎J]overR[I] - asHomOverR = Iso.fun isoR (R [ I ⊎ J ]) + asHomOverR = Iso.fun isoR (R [ I ⊎ J ]) - ≡RingHoms : snd asHomOverR[I] ∘r baseRingHom ≡ baseRingHom + ≡RingHoms : snd asHomOverR[I] ∘r baseRingHom ≡ baseRingHom ≡RingHoms = RingHom≡ (funExt λ x → - fst (snd asHomOverR[I] ∘r baseRingHom) x ≡⟨⟩ - fst (snd asHomOverR[I]) (const x · 1a) ≡⟨⟩ - (const x · 1a) ⋆ 1a ≡⟨ cong (_⋆ 1a) (·IdR (const x)) ⟩ - const x ⋆ 1a ≡⟨⟩ - (fst ψ (const x)) · 1a ≡⟨⟩ - (const x · const 1r) · 1a ≡⟨ cong (_· 1a) (·IdR (const x)) ⟩ - const x · 1a ∎) + fst (snd asHomOverR[I] ∘r baseRingHom) x ≡⟨⟩ + fst (snd asHomOverR[I]) (const x · 1a) ≡⟨⟩ + (const x · 1a) ⋆ 1a ≡⟨ cong (_⋆ 1a) (·IdR (const x)) ⟩ + const x ⋆ 1a ≡⟨⟩ + (fst ψ (const x)) · 1a ≡⟨⟩ + (const x · const 1r) · 1a ≡⟨ cong (_· 1a) (·IdR (const x)) ⟩ + const x · 1a ∎) ≡R[I⊎J] = - baseChange baseRingHom R[I⊎J]overR[I] ≡⟨⟩ - Iso.inv isoR ((CommAlgebra→CommRing R[I⊎J]overR[I]) , (snd asHomOverR[I]) ∘r baseRingHom) ≡⟨ step1 ⟩ - Iso.inv isoR (CommAlgebra→CommRing (R [ I ⊎ J ]) , baseRingHom) ≡⟨⟩ + baseChange baseRingHom R[I⊎J]overR[I] ≡⟨⟩ + Iso.inv isoR ((CommAlgebra→CommRing R[I⊎J]overR[I]) , (snd asHomOverR[I]) ∘r baseRingHom) ≡⟨ step1 ⟩ + Iso.inv isoR (CommAlgebra→CommRing (R [ I ⊎ J ]) , baseRingHom) ≡⟨⟩ Iso.inv isoR asHomOverR ≡⟨ step2 ⟩ - R [ I ⊎ J ] ∎ + R [ I ⊎ J ] ∎ where - step1 : Iso.inv isoR ((CommAlgebra→CommRing R[I⊎J]overR[I]) , (snd asHomOverR[I]) ∘r baseRingHom) - ≡ Iso.inv isoR (CommAlgebra→CommRing (R [ I ⊎ J ]) , baseRingHom) + step1 : Iso.inv isoR ((CommAlgebra→CommRing R[I⊎J]overR[I]) , (snd asHomOverR[I]) ∘r baseRingHom) + ≡ Iso.inv isoR (CommAlgebra→CommRing (R [ I ⊎ J ]) , baseRingHom) step1 i = Iso.inv isoR ((CommAlgebra→CommRing R[I⊎J]overR[I]) , ≡RingHoms i) - step2 = Iso.leftInv isoR (R [ I ⊎ J ]) + step2 = Iso.leftInv isoR (R [ I ⊎ J ]) fst≡R[I⊎J] : cong fst ≡R[I⊎J] ≡ refl fst≡R[I⊎J] = @@ -110,16 +110,16 @@ refl ∎ fromOverR[I] : CommAlgebraHom R[I][J]overR[I] R[I⊎J]overR[I] - fromOverR[I] = inducedHom R[I⊎J]overR[I] (λ j → var (inr j)) + fromOverR[I] = inducedHom R[I⊎J]overR[I] (λ j → var (inr j)) - from' : CommAlgebraHom R[I][J] (baseChange baseRingHom R[I⊎J]overR[I]) + from' : CommAlgebraHom R[I][J] (baseChange baseRingHom R[I⊎J]overR[I]) from' = baseChangeHom {S = R} - baseRingHom + baseRingHom R[I][J]overR[I] R[I⊎J]overR[I] fromOverR[I] - from : CommAlgebraHom R[I][J] (R [ I ⊎ J ]) + from : CommAlgebraHom R[I][J] (R [ I ⊎ J ]) from = subst (CommAlgebraHom R[I][J]) ≡R[I⊎J] from' @@ -130,42 +130,42 @@ -} incVar : (x : I ⊎ J) → ⟨ R[I][J] ⟩ - incVar (inl i) = const (var i) - incVar (inr j) = var j + incVar (inl i) = const (var i) + incVar (inr j) = var j - toOnGenerators : (x : I ⊎ J) → fst to (var x) ≡ incVar x + toOnGenerators : (x : I ⊎ J) → fst to (var x) ≡ incVar x toOnGenerators (inl i) = refl toOnGenerators (inr j) = refl - fromOnGenerators : (x : I ⊎ J) → fst from (incVar x) ≡ (var x) + fromOnGenerators : (x : I ⊎ J) → fst from (incVar x) ≡ (var x) fromOnGenerators (inl i) = - fst from (const (var i)) ≡⟨⟩ - (subst (λ X → ⟨ R[I][J] ⟩ → X) (cong fst ≡R[I⊎J]) (fst from')) (const (var i)) ≡⟨ step1 ⟩ - (subst (λ X → ⟨ R[I][J] ⟩ → X) refl (fst from')) (const (var i)) ≡⟨ step2 ⟩ - (fst from') (const (var i)) ≡⟨⟩ - var (inl i) · 1a ≡⟨ ·IdR _ ⟩ - var (inl i) ∎ + fst from (const (var i)) ≡⟨⟩ + (subst (λ X → ⟨ R[I][J] ⟩ → X) (cong fst ≡R[I⊎J]) (fst from')) (const (var i)) ≡⟨ step1 ⟩ + (subst (λ X → ⟨ R[I][J] ⟩ → X) refl (fst from')) (const (var i)) ≡⟨ step2 ⟩ + (fst from') (const (var i)) ≡⟨⟩ + var (inl i) · 1a ≡⟨ ·IdR _ ⟩ + var (inl i) ∎ where step1 : _ ≡ _ - step1 = cong (λ u → subst (λ X → ⟨ R[I][J] ⟩ → X) u (fst from') (const (var i))) fst≡R[I⊎J] + step1 = cong (λ u → subst (λ X → ⟨ R[I][J] ⟩ → X) u (fst from') (const (var i))) fst≡R[I⊎J] step2 : _ ≡ _ - step2 = cong (λ u → u (const (var i))) + step2 = cong (λ u → u (const (var i))) (substRefl {B = λ (X : Type ℓ) → ⟨ R[I][J] ⟩ → X} (fst from')) fromOnGenerators (inr j) = - fst from (var j) ≡⟨⟩ - (subst (λ X → ⟨ R[I][J] ⟩ → X) (cong fst ≡R[I⊎J]) (fst from')) (var j) ≡⟨ step1 ⟩ - (subst (λ X → ⟨ R[I][J] ⟩ → X) refl (fst from')) (var j) ≡⟨ step2 ⟩ - (fst from') (var j) ≡⟨⟩ - (var (inr j)) ∎ - where step1 = cong (λ u → subst (λ X → ⟨ R[I][J] ⟩ → X) u (fst from') (var j)) fst≡R[I⊎J] - step2 = cong (λ u → u (var j)) + fst from (var j) ≡⟨⟩ + (subst (λ X → ⟨ R[I][J] ⟩ → X) (cong fst ≡R[I⊎J]) (fst from')) (var j) ≡⟨ step1 ⟩ + (subst (λ X → ⟨ R[I][J] ⟩ → X) refl (fst from')) (var j) ≡⟨ step2 ⟩ + (fst from') (var j) ≡⟨⟩ + (var (inr j)) ∎ + where step1 = cong (λ u → subst (λ X → ⟨ R[I][J] ⟩ → X) u (fst from') (var j)) fst≡R[I⊎J] + step2 = cong (λ u → u (var j)) (substRefl {B = λ (X : Type ℓ) → ⟨ R[I][J] ⟩ → X} (fst from')) open AlgebraHoms - fromTo : (x : ⟨ R [ I ⊎ J ] ⟩) → fst (from ∘a to) x ≡ x - fromTo = isIdByUMP (from ∘a to) - λ x → fst (from ∘a to) (var x) ≡⟨ cong (λ u → fst from u) (toOnGenerators x) ⟩ + fromTo : (x : ⟨ R [ I ⊎ J ] ⟩) → fst (from ∘a to) x ≡ x + fromTo = isIdByUMP (from ∘a to) + λ x → fst (from ∘a to) (var x) ≡⟨ cong (λ u → fst from u) (toOnGenerators x) ⟩ fst from (incVar x) ≡⟨ fromOnGenerators x ⟩ - var x ∎ + var x ∎ {- For 'to ∘a from', we need 'to' and 'from' as homomorphisms of R[I]-algebras. @@ -190,7 +190,7 @@ fst to (r ⋆ x) ≡⟨⟩ fst to (fst ψ r · x) ≡⟨ z .pres· (fst ψ r) x ⟩ fst to (fst ψ r) · fst to x ≡⟨ cong (_· fst to x) (to∘ψ≡const r) ⟩ - const r · fst to x ≡⟨⟩ + const r · fst to x ≡⟨⟩ (r ⋆ fst to x) ∎ where {- @@ -203,40 +203,40 @@ To do that, we have to show that const is an R-algebra homomorphism -} - open Construction using (+HomConst; ·HomConst) - constHom : CommAlgebraHom (R [ I ]) R[I][J] - constHom .fst = const + open Construction using (+HomConst; ·HomConst) + constHom : CommAlgebraHom (R [ I ]) R[I][J] + constHom .fst = const constHom .snd = makeIsAlgebraHom refl - +HomConst - ·HomConst + +HomConst + ·HomConst λ r x → - const (const r · x) ≡⟨ ·HomConst (const r) x ⟩ - const (const r) · const x ≡[ i ]⟨ - const (sym (·IdR (const r)) i) · const x ⟩ - const (const r · const 1r) · const x ≡[ i ]⟨ - sym (·IdR (const (const r · const 1r))) i - · const x ⟩ - (const (const r · const 1r) · const (const 1r)) · const x ≡⟨⟩ - CommAlgebraStr._⋆_ (snd R[I][J]) r (const x) ∎ - - to∘ψOnVar : (i : I) → fst (to ∘a ψOverR) (var i) ≡ const (var i) + const (const r · x) ≡⟨ ·HomConst (const r) x ⟩ + const (const r) · const x ≡[ i ]⟨ + const (sym (·IdR (const r)) i) · const x ⟩ + const (const r · const 1r) · const x ≡[ i ]⟨ + sym (·IdR (const (const r · const 1r))) i + · const x ⟩ + (const (const r · const 1r) · const (const 1r)) · const x ≡⟨⟩ + CommAlgebraStr._⋆_ (snd R[I][J]) r (const x) ∎ + + to∘ψOnVar : (i : I) → fst (to ∘a ψOverR) (var i) ≡ const (var i) to∘ψOnVar i = refl - to∘ψ≡const : (x : ⟨ R [ I ] ⟩) → fst to (fst ψ x) ≡ const x + to∘ψ≡const : (x : ⟨ R [ I ] ⟩) → fst to (fst ψ x) ≡ const x to∘ψ≡const = - equalByUMP R[I][J] (to ∘a ψOverR) constHom to∘ψOnVar + equalByUMP R[I][J] (to ∘a ψOverR) constHom to∘ψOnVar toFromOverR[I] : (x : ⟨ R[I][J]overR[I] ⟩) → fst (toOverR[I] ∘a fromOverR[I]) x ≡ x - toFromOverR[I] = isIdByUMP (toOverR[I] ∘a fromOverR[I]) λ _ → refl + toFromOverR[I] = isIdByUMP (toOverR[I] ∘a fromOverR[I]) λ _ → refl {- export bundled results -} module _ {R : CommRing ℓ} {I J : Type ℓ} where open CalculateFreeCommAlgebraOnCoproduct R I J - equivFreeCommSum : CommAlgebraEquiv (R [ I ⊎ J ]) R[I][J] + equivFreeCommSum : CommAlgebraEquiv (R [ I ⊎ J ]) R[I][J] equivFreeCommSum = (biInvEquiv→Equiv-left asBiInv) , snd to where open BiInvEquiv diff --git a/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html b/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html index 91bd07d0cd..bc688a7b9d 100644 --- a/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html +++ b/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html @@ -2,461 +2,475 @@ Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties
{-# OPTIONS --safe #-}
 
 module Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties where
-
-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.FreeCommAlgebra.Base
-open import Cubical.Algebra.Ring        using ()
-open import Cubical.Algebra.CommAlgebra
-open import Cubical.Algebra.CommAlgebra.Instances.Initial
-open import Cubical.Algebra.Algebra
-
-open import Cubical.Data.Empty
-open import Cubical.Data.Sigma
-
-private
-  variable
-    ℓ ℓ' ℓ'' : Level
-
-module Theory {R : CommRing ℓ} {I : Type ℓ'} where
-  open CommRingStr (snd R)
-         using (0r; 1r)
-         renaming (_·_ to _·r_; _+_ to _+r_; ·Comm to ·r-comm; ·IdR to ·r-rid)
-
-  module _ (A : CommAlgebra R ℓ'') (φ : I → ⟨ A ⟩) where
-    open CommAlgebraStr (A .snd)
-    open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra A)
-    open Construction using (var; const) renaming (_+_ to _+c_; -_ to -c_; _·_ to _·c_)
-
-    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 (Construction.+-assoc P Q S i) = +Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i
-    inducedMap (Construction.+-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 (Construction.+-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 (Construction.+-comm P Q i) = +Comm (inducedMap P) (inducedMap Q) i
-    inducedMap (P ·c Q) = inducedMap P · inducedMap Q
-    inducedMap (Construction.·-assoc P Q S i) = ·Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i
-    inducedMap (Construction.·-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 (Construction.·-comm P Q i) = ·Comm (inducedMap P) (inducedMap Q) i
-    inducedMap (Construction.ldist P Q S i) = ·DistL+ (inducedMap P) (inducedMap Q) (inducedMap S) i
-    inducedMap (Construction.+HomConst s t i) = ⋆DistL+ s t 1a i
-    inducedMap (Construction.·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 (Construction.0-trunc P Q p q i j) =
-      isSetAlgebra (CommAlgebra→Algebra A) (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 ∎
-
-  module _ (A : CommAlgebra R ℓ'') where
-    open CommAlgebraStr (A .snd)
-    open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra A)
-    open Construction using (var; const) renaming (_+_ to _+c_; -_ to -c_; _·_ to _·c_)
-
-    Hom = CommAlgebraHom  (R [ I ]) A
-    open IsAlgebraHom
-
-    evaluateAt : Hom → I → ⟨ A ⟩
-    evaluateAt φ x = φ .fst (var x)
-
-    mapRetrievable : ∀ (φ : I → ⟨ A ⟩)
-                     → evaluateAt (inducedHom A φ) ≡ φ
-    mapRetrievable φ = refl
-
-    proveEq : ∀ {X : Type ℓ''} (isSetX : isSet X) (f g : ⟨ R [ I ] ⟩ → X)
-              → (var-eq : (x : I) → f (var x) ≡ g (var x))
-              → (const-eq : (r : ⟨ R ⟩) → f (const r) ≡ g (const r))
-              → (+-eq : (x y : ⟨ R [ I ] ⟩) → (eq-x : f x ≡ g x) → (eq-y : f y ≡ g y)
-                        → f (x +c y) ≡ g (x +c y))
-              → (·-eq : (x y : ⟨ R [ I ] ⟩) → (eq-x : f x ≡ g x) → (eq-y : f y ≡ g y)
-                        → f (x ·c y) ≡ g (x ·c y))
-              → (-eq : (x : ⟨ R [ I ] ⟩) → (eq-x : f x ≡ g x)
-                        → f (-c x) ≡ g (-c x))
-              → f ≡ g
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (var x) = var-eq x i
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (const x) = const-eq x i
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (x +c y) =
-      +-eq x y
-           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
-           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i y)
-           i
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (-c x) =
-      -eq x ((λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)) i
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (x ·c y) =
-      ·-eq x y
-           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
-           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i y)
-           i
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-assoc x y z j) =
-       let
-        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
-        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
-        a₀₋ : f (x +c (y +c z)) ≡ g (x +c (y +c z))
-        a₀₋ = +-eq _ _ (rec x) (+-eq _ _ (rec y) (rec z))
-        a₁₋ : f ((x +c y) +c z) ≡ g ((x +c y) +c z)
-        a₁₋ = +-eq _ _ (+-eq _ _ (rec x) (rec y)) (rec z)
-        a₋₀ : f (x +c (y +c z)) ≡ f ((x +c y) +c z)
-        a₋₀ = cong f (Construction.+-assoc x y z)
-        a₋₁ : g (x +c (y +c z)) ≡ g ((x +c y) +c z)
-        a₋₁ = cong g (Construction.+-assoc x y z)
-      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
-
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-rid x j) =
-       let
-        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
-        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
-        a₀₋ : f (x +c (const 0r)) ≡ g (x +c (const 0r))
-        a₀₋ = +-eq _ _ (rec x) (const-eq 0r)
-        a₁₋ : f x ≡ g x
-        a₁₋ = rec x
-        a₋₀ : f (x +c (const 0r)) ≡ f x
-        a₋₀ = cong f (Construction.+-rid x)
-        a₋₁ : g (x +c (const 0r)) ≡ g x
-        a₋₁ = cong g (Construction.+-rid x)
-      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
-
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-rinv x j) =
-       let
-        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
-        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
-        a₀₋ : f (x +c (-c x)) ≡ g (x +c (-c x))
-        a₀₋ = +-eq x (-c x) (rec x) (-eq x (rec x))
-        a₁₋ : f (const 0r) ≡ g (const 0r)
-        a₁₋ = const-eq 0r
-        a₋₀ : f (x +c (-c x)) ≡ f (const 0r)
-        a₋₀ = cong f (Construction.+-rinv x)
-        a₋₁ : g (x +c (-c x)) ≡ g (const 0r)
-        a₋₁ = cong g (Construction.+-rinv x)
-      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
-
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-comm x y j) =
-      let
-        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
-        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
-        a₀₋ : f (x +c y) ≡ g (x +c y)
-        a₀₋ = +-eq x y (rec x) (rec y)
-        a₁₋ : f (y +c x) ≡ g (y +c x)
-        a₁₋ = +-eq y x (rec y) (rec x)
-        a₋₀ : f (x +c y) ≡ f (y +c x)
-        a₋₀ = cong f (Construction.+-comm x y)
-        a₋₁ : g (x +c y) ≡ g (y +c x)
-        a₋₁ = cong g (Construction.+-comm x y)
-      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
-
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·-assoc x y z j) =
-       let
-        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
-        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
-        a₀₋ : f (x ·c (y ·c z)) ≡ g (x ·c (y ·c z))
-        a₀₋ = ·-eq _ _ (rec x) (·-eq _ _ (rec y) (rec z))
-        a₁₋ : f ((x ·c y) ·c z) ≡ g ((x ·c y) ·c z)
-        a₁₋ = ·-eq _ _ (·-eq _ _ (rec x) (rec y)) (rec z)
-        a₋₀ : f (x ·c (y ·c z)) ≡ f ((x ·c y) ·c z)
-        a₋₀ = cong f (Construction.·-assoc x y z)
-        a₋₁ : g (x ·c (y ·c z)) ≡ g ((x ·c y) ·c z)
-        a₋₁ = cong g (Construction.·-assoc x y z)
-      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
-
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·-lid x j) =
-       let
-        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
-        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
-        a₀₋ : f ((const 1r) ·c x) ≡ g ((const 1r) ·c x)
-        a₀₋ = ·-eq _ _ (const-eq 1r) (rec x)
-        a₁₋ : f x ≡ g x
-        a₁₋ = rec x
-        a₋₀ : f ((const 1r) ·c x) ≡ f x
-        a₋₀ = cong f (Construction.·-lid x)
-        a₋₁ : g ((const 1r) ·c x) ≡ g x
-        a₋₁ = cong g (Construction.·-lid x)
-      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
-
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·-comm x y j) =
-       let
-        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
-        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
-        a₀₋ : f (x ·c y) ≡ g (x ·c y)
-        a₀₋ = ·-eq _ _ (rec x) (rec y)
-        a₁₋ : f (y ·c x) ≡ g (y ·c x)
-        a₁₋ = ·-eq _ _ (rec y) (rec x)
-        a₋₀ : f (x ·c y) ≡ f (y ·c x)
-        a₋₀ = cong f (Construction.·-comm x y)
-        a₋₁ : g (x ·c y) ≡ g (y ·c x)
-        a₋₁ = cong g (Construction.·-comm x y)
-      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
-
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.ldist x y z j) =
-       let
-        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
-        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
-        a₀₋ : f ((x +c y) ·c z) ≡ g ((x +c y) ·c z)
-        a₀₋ = ·-eq (x +c y) z
-           (+-eq _ _ (rec x) (rec y))
-           (rec z)
-        a₁₋ : f ((x ·c z) +c (y ·c z)) ≡ g ((x ·c z) +c (y ·c z))
-        a₁₋ = +-eq _ _ (·-eq _ _ (rec x) (rec z)) (·-eq _ _ (rec y) (rec z))
-        a₋₀ : f ((x +c y) ·c z) ≡ f ((x ·c z) +c (y ·c z))
-        a₋₀ = cong f (Construction.ldist x y z)
-        a₋₁ : g ((x +c y) ·c z) ≡ g ((x ·c z) +c (y ·c z))
-        a₋₁ = cong g (Construction.ldist x y z)
-      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
-
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+HomConst s t j) =
-       let
-        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
-        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
-        a₀₋ : f (const (s +r t)) ≡ g (const (s +r t))
-        a₀₋ = const-eq (s +r t)
-        a₁₋ : f (const s +c const t) ≡ g (const s +c const t)
-        a₁₋ = +-eq _ _ (const-eq s) (const-eq t)
-        a₋₀ : f (const (s +r t)) ≡ f (const s +c const t)
-        a₋₀ = cong f (Construction.+HomConst s t)
-        a₋₁ : g (const (s +r t)) ≡ g (const s +c const t)
-        a₋₁ = cong g (Construction.+HomConst s t)
-      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
-
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·HomConst s t j) =
-       let
-        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
-        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
-        a₀₋ : f (const (s ·r t)) ≡ g (const (s ·r t))
-        a₀₋ = const-eq (s ·r t)
-        a₁₋ : f (const s ·c const t) ≡ g (const s ·c const t)
-        a₁₋ = ·-eq _ _ (const-eq s) (const-eq t)
-        a₋₀ : f (const (s ·r t)) ≡ f (const s ·c const t)
-        a₋₀ = cong f (Construction.·HomConst s t)
-        a₋₁ : g (const (s ·r t)) ≡ g (const s ·c const t)
-        a₋₁ = cong g (Construction.·HomConst s t)
-      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
-
-    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.0-trunc x y p q j k) =
-      let
-        P : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
-        P x i = proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x
-        Q : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
-        Q x i = proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x
-      in isOfHLevel→isOfHLevelDep 2
-           (λ z → isProp→isSet (isSetX (f z) (g z))) _ _
-           (cong P p)
-           (cong Q q)
-           (Construction.0-trunc x y p q) j k i
-
-
-    homRetrievable : ∀ (f : Hom)
-                     → inducedMap A (evaluateAt f) ≡ fst f
-    homRetrievable f =
-       proveEq
-        (isSetAlgebra (CommAlgebra→Algebra A))
-        (inducedMap A (evaluateAt f))
-        (λ x → f $a x)
-        (λ 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 (Construction.·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) ∎)
-       (λ x eq-x →
-           ι (-c x)    ≡⟨ refl ⟩
-           - ι x       ≡⟨ cong (λ u → - u) eq-x ⟩
-           - (f $a x)  ≡⟨ sym (f.pres- x) ⟩
-           f $a (-c x) ∎)
-      where
-      ι = 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)
-
-inducedHom : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'')
-             (φ : I → fst A )
-             → CommAlgebraHom (R [ I ]) A
-inducedHom A φ = Theory.inducedHom A φ
-
-
-homMapIso : {R : CommRing ℓ} {I : Type ℓ''} (A : CommAlgebra R ℓ')
-             → Iso (CommAlgebraHom (R [ I ]) A) (I → (fst A))
-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)
-
-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 ≡ inducedHom A φ
-inducedHomUnique {I = I} A φ f p =
-  isoFunInjective (homMapIso A) f (inducedHom A φ) λ j i → p i j
-
-homMapPath : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R (ℓ-max ℓ ℓ'))
-             → CommAlgebraHom (R [ I ]) A ≡ (I → fst A)
-homMapPath A = isoToPath (homMapIso A)
-
-{- Corollary: Two homomorphisms with the same values on generators are equal -}
-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))
-           → (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
-
-{- A corollary, which is useful for constructing isomorphisms to
+{-
+  This file contains
+  * definitions of the induced maps appearing in the universal property of R[I],
+    that is:  * for any map I → A, where A is a commutative R-algebra,
+                the induced algebra homomorphism R[I] → A
+                ('inducedHom')
+              * for any hom R[I] → A, the 'restricttion to variables' I → A
+                ('evaluateAt')
+  * a proof that the two constructions are inverse to each other
+    ('homMapIso')
+  * proofs that the constructions are natural in various ways
+  * a proof that the FreeCommAlgebra on zero generators is the initial R-Algebra
+    ('freeOn⊥')
+-}
+
+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.FreeCommAlgebra.Base
+open import Cubical.Algebra.Ring        using ()
+open import Cubical.Algebra.CommAlgebra
+open import Cubical.Algebra.CommAlgebra.Instances.Initial
+open import Cubical.Algebra.Algebra
+
+open import Cubical.Data.Empty
+open import Cubical.Data.Sigma
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+module Theory {R : CommRing ℓ} {I : Type ℓ'} where
+  open CommRingStr (snd R)
+         using (0r; 1r)
+         renaming (_·_ to _·r_; _+_ to _+r_; ·Comm to ·r-comm; ·IdR to ·r-rid)
+
+  module _ (A : CommAlgebra R ℓ'') (φ : I → ⟨ A ⟩) where
+    open CommAlgebraStr (A .snd)
+    open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra A)
+    open Construction using (var; const) renaming (_+_ to _+c_; -_ to -c_; _·_ to _·c_)
+
+    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 (Construction.+-assoc P Q S i) = +Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i
+    inducedMap (Construction.+-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 (Construction.+-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 (Construction.+-comm P Q i) = +Comm (inducedMap P) (inducedMap Q) i
+    inducedMap (P ·c Q) = inducedMap P · inducedMap Q
+    inducedMap (Construction.·-assoc P Q S i) = ·Assoc (inducedMap P) (inducedMap Q) (inducedMap S) i
+    inducedMap (Construction.·-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 (Construction.·-comm P Q i) = ·Comm (inducedMap P) (inducedMap Q) i
+    inducedMap (Construction.ldist P Q S i) = ·DistL+ (inducedMap P) (inducedMap Q) (inducedMap S) i
+    inducedMap (Construction.+HomConst s t i) = ⋆DistL+ s t 1a i
+    inducedMap (Construction.·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 (Construction.0-trunc P Q p q i j) =
+      isSetAlgebra (CommAlgebra→Algebra A) (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 ∎
+
+  module _ (A : CommAlgebra R ℓ'') where
+    open CommAlgebraStr (A .snd)
+    open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra A)
+    open Construction using (var; const) renaming (_+_ to _+c_; -_ to -c_; _·_ to _·c_)
+
+    Hom = CommAlgebraHom  (R [ I ]) A
+    open IsAlgebraHom
+
+    evaluateAt : Hom → I → ⟨ A ⟩
+    evaluateAt φ x = φ .fst (var x)
+
+    mapRetrievable : ∀ (φ : I → ⟨ A ⟩)
+                     → evaluateAt (inducedHom A φ) ≡ φ
+    mapRetrievable φ = refl
+
+    proveEq : ∀ {X : Type ℓ''} (isSetX : isSet X) (f g : ⟨ R [ I ] ⟩ → X)
+              → (var-eq : (x : I) → f (var x) ≡ g (var x))
+              → (const-eq : (r : ⟨ R ⟩) → f (const r) ≡ g (const r))
+              → (+-eq : (x y : ⟨ R [ I ] ⟩) → (eq-x : f x ≡ g x) → (eq-y : f y ≡ g y)
+                        → f (x +c y) ≡ g (x +c y))
+              → (·-eq : (x y : ⟨ R [ I ] ⟩) → (eq-x : f x ≡ g x) → (eq-y : f y ≡ g y)
+                        → f (x ·c y) ≡ g (x ·c y))
+              → (-eq : (x : ⟨ R [ I ] ⟩) → (eq-x : f x ≡ g x)
+                        → f (-c x) ≡ g (-c x))
+              → f ≡ g
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (var x) = var-eq x i
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (const x) = const-eq x i
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (x +c y) =
+      +-eq x y
+           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
+           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i y)
+           i
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (-c x) =
+      -eq x ((λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)) i
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (x ·c y) =
+      ·-eq x y
+           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
+           (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i y)
+           i
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-assoc x y z j) =
+       let
+        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
+        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
+        a₀₋ : f (x +c (y +c z)) ≡ g (x +c (y +c z))
+        a₀₋ = +-eq _ _ (rec x) (+-eq _ _ (rec y) (rec z))
+        a₁₋ : f ((x +c y) +c z) ≡ g ((x +c y) +c z)
+        a₁₋ = +-eq _ _ (+-eq _ _ (rec x) (rec y)) (rec z)
+        a₋₀ : f (x +c (y +c z)) ≡ f ((x +c y) +c z)
+        a₋₀ = cong f (Construction.+-assoc x y z)
+        a₋₁ : g (x +c (y +c z)) ≡ g ((x +c y) +c z)
+        a₋₁ = cong g (Construction.+-assoc x y z)
+      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
+
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-rid x j) =
+       let
+        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
+        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
+        a₀₋ : f (x +c (const 0r)) ≡ g (x +c (const 0r))
+        a₀₋ = +-eq _ _ (rec x) (const-eq 0r)
+        a₁₋ : f x ≡ g x
+        a₁₋ = rec x
+        a₋₀ : f (x +c (const 0r)) ≡ f x
+        a₋₀ = cong f (Construction.+-rid x)
+        a₋₁ : g (x +c (const 0r)) ≡ g x
+        a₋₁ = cong g (Construction.+-rid x)
+      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
+
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-rinv x j) =
+       let
+        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
+        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
+        a₀₋ : f (x +c (-c x)) ≡ g (x +c (-c x))
+        a₀₋ = +-eq x (-c x) (rec x) (-eq x (rec x))
+        a₁₋ : f (const 0r) ≡ g (const 0r)
+        a₁₋ = const-eq 0r
+        a₋₀ : f (x +c (-c x)) ≡ f (const 0r)
+        a₋₀ = cong f (Construction.+-rinv x)
+        a₋₁ : g (x +c (-c x)) ≡ g (const 0r)
+        a₋₁ = cong g (Construction.+-rinv x)
+      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
+
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+-comm x y j) =
+      let
+        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
+        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
+        a₀₋ : f (x +c y) ≡ g (x +c y)
+        a₀₋ = +-eq x y (rec x) (rec y)
+        a₁₋ : f (y +c x) ≡ g (y +c x)
+        a₁₋ = +-eq y x (rec y) (rec x)
+        a₋₀ : f (x +c y) ≡ f (y +c x)
+        a₋₀ = cong f (Construction.+-comm x y)
+        a₋₁ : g (x +c y) ≡ g (y +c x)
+        a₋₁ = cong g (Construction.+-comm x y)
+      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
+
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·-assoc x y z j) =
+       let
+        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
+        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
+        a₀₋ : f (x ·c (y ·c z)) ≡ g (x ·c (y ·c z))
+        a₀₋ = ·-eq _ _ (rec x) (·-eq _ _ (rec y) (rec z))
+        a₁₋ : f ((x ·c y) ·c z) ≡ g ((x ·c y) ·c z)
+        a₁₋ = ·-eq _ _ (·-eq _ _ (rec x) (rec y)) (rec z)
+        a₋₀ : f (x ·c (y ·c z)) ≡ f ((x ·c y) ·c z)
+        a₋₀ = cong f (Construction.·-assoc x y z)
+        a₋₁ : g (x ·c (y ·c z)) ≡ g ((x ·c y) ·c z)
+        a₋₁ = cong g (Construction.·-assoc x y z)
+      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
+
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·-lid x j) =
+       let
+        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
+        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
+        a₀₋ : f ((const 1r) ·c x) ≡ g ((const 1r) ·c x)
+        a₀₋ = ·-eq _ _ (const-eq 1r) (rec x)
+        a₁₋ : f x ≡ g x
+        a₁₋ = rec x
+        a₋₀ : f ((const 1r) ·c x) ≡ f x
+        a₋₀ = cong f (Construction.·-lid x)
+        a₋₁ : g ((const 1r) ·c x) ≡ g x
+        a₋₁ = cong g (Construction.·-lid x)
+      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
+
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·-comm x y j) =
+       let
+        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
+        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
+        a₀₋ : f (x ·c y) ≡ g (x ·c y)
+        a₀₋ = ·-eq _ _ (rec x) (rec y)
+        a₁₋ : f (y ·c x) ≡ g (y ·c x)
+        a₁₋ = ·-eq _ _ (rec y) (rec x)
+        a₋₀ : f (x ·c y) ≡ f (y ·c x)
+        a₋₀ = cong f (Construction.·-comm x y)
+        a₋₁ : g (x ·c y) ≡ g (y ·c x)
+        a₋₁ = cong g (Construction.·-comm x y)
+      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
+
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.ldist x y z j) =
+       let
+        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
+        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
+        a₀₋ : f ((x +c y) ·c z) ≡ g ((x +c y) ·c z)
+        a₀₋ = ·-eq (x +c y) z
+           (+-eq _ _ (rec x) (rec y))
+           (rec z)
+        a₁₋ : f ((x ·c z) +c (y ·c z)) ≡ g ((x ·c z) +c (y ·c z))
+        a₁₋ = +-eq _ _ (·-eq _ _ (rec x) (rec z)) (·-eq _ _ (rec y) (rec z))
+        a₋₀ : f ((x +c y) ·c z) ≡ f ((x ·c z) +c (y ·c z))
+        a₋₀ = cong f (Construction.ldist x y z)
+        a₋₁ : g ((x +c y) ·c z) ≡ g ((x ·c z) +c (y ·c z))
+        a₋₁ = cong g (Construction.ldist x y z)
+      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
+
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.+HomConst s t j) =
+       let
+        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
+        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
+        a₀₋ : f (const (s +r t)) ≡ g (const (s +r t))
+        a₀₋ = const-eq (s +r t)
+        a₁₋ : f (const s +c const t) ≡ g (const s +c const t)
+        a₁₋ = +-eq _ _ (const-eq s) (const-eq t)
+        a₋₀ : f (const (s +r t)) ≡ f (const s +c const t)
+        a₋₀ = cong f (Construction.+HomConst s t)
+        a₋₁ : g (const (s +r t)) ≡ g (const s +c const t)
+        a₋₁ = cong g (Construction.+HomConst s t)
+      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
+
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.·HomConst s t j) =
+       let
+        rec : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
+        rec x = (λ i → proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x)
+        a₀₋ : f (const (s ·r t)) ≡ g (const (s ·r t))
+        a₀₋ = const-eq (s ·r t)
+        a₁₋ : f (const s ·c const t) ≡ g (const s ·c const t)
+        a₁₋ = ·-eq _ _ (const-eq s) (const-eq t)
+        a₋₀ : f (const (s ·r t)) ≡ f (const s ·c const t)
+        a₋₀ = cong f (Construction.·HomConst s t)
+        a₋₁ : g (const (s ·r t)) ≡ g (const s ·c const t)
+        a₋₁ = cong g (Construction.·HomConst s t)
+      in isSet→isSet' isSetX a₀₋ a₁₋ a₋₀ a₋₁ j i
+
+    proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i (Construction.0-trunc x y p q j k) =
+      let
+        P : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
+        P x i = proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x
+        Q : (x : ⟨ R [ I ] ⟩) → f x ≡ g x
+        Q x i = proveEq isSetX f g var-eq const-eq +-eq ·-eq -eq i x
+      in isOfHLevel→isOfHLevelDep 2
+           (λ z → isProp→isSet (isSetX (f z) (g z))) _ _
+           (cong P p)
+           (cong Q q)
+           (Construction.0-trunc x y p q) j k i
+
+
+    homRetrievable : ∀ (f : Hom)
+                     → inducedMap A (evaluateAt f) ≡ fst f
+    homRetrievable f =
+       proveEq
+        (isSetAlgebra (CommAlgebra→Algebra A))
+        (inducedMap A (evaluateAt f))
+        (λ x → f $a x)
+        (λ 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 (Construction.·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) ∎)
+       (λ x eq-x →
+           ι (-c x)    ≡⟨ refl ⟩
+           - ι x       ≡⟨ cong (λ u → - u) eq-x ⟩
+           - (f $a x)  ≡⟨ sym (f.pres- x) ⟩
+           f $a (-c x) ∎)
+      where
+      ι = 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)
+
+inducedHom : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'')
+             (φ : I → fst A )
+             → CommAlgebraHom (R [ I ]) A
+inducedHom A φ = Theory.inducedHom A φ
+
+
+homMapIso : {R : CommRing ℓ} {I : Type ℓ''} (A : CommAlgebra R ℓ')
+             → Iso (CommAlgebraHom (R [ I ]) A) (I → (fst A))
+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)
+
+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 ≡ inducedHom A φ
+inducedHomUnique {I = I} A φ f p =
+  isoFunInjective (homMapIso A) f (inducedHom A φ) λ j i → p i j
+
+homMapPath : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R (ℓ-max ℓ ℓ'))
+             → CommAlgebraHom (R [ I ]) A ≡ (I → fst A)
+homMapPath A = isoToPath (homMapIso A)
+
+{- Corollary: Two homomorphisms with the same values on generators are equal -}
+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))
+           → (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
+
+{- A corollary, which is useful for constructing isomorphisms to
    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)
-          → (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
-
-module _ {R : CommRing ℓ} {A B : CommAlgebra R ℓ''} where
-  open AlgebraHoms
-  A′ = CommAlgebra→Algebra A
-  B′ = CommAlgebra→Algebra B
-  R′ = (CommRing→Ring R)
-  ν : AlgebraHom A′ B′ → (⟨ A ⟩ → ⟨ B ⟩)
-  ν φ = φ .fst
-
-  {-
+isIdByUMP : {R : CommRing ℓ} {I : Type ℓ'}
+          → (f : CommAlgebraHom (R [ I ]) (R [ I ]))
+          → ((i : I) → fst f (Construction.var i) ≡ Construction.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
+
+module _ {R : CommRing ℓ} {A B : CommAlgebra R ℓ''} where
+  open AlgebraHoms
+  A′ = CommAlgebra→Algebra A
+  B′ = CommAlgebra→Algebra B
+  R′ = (CommRing→Ring R)
+  ν : AlgebraHom A′ B′ → (⟨ A ⟩ → ⟨ B ⟩)
+  ν φ = φ .fst
+
+  {-
     Hom(R[I],A) → (I → A)
          ↓          ↓ψ
     Hom(R[I],B) → (I → B)
   -}
-  naturalEvR : {I : Type ℓ'} (ψ : CommAlgebraHom A B)
-             (f : CommAlgebraHom (R [ I ]) A)
-             → (fst ψ) ∘ evaluateAt A f ≡ evaluateAt B (ψ ∘a f)
-  naturalEvR ψ f = refl
+  naturalEvR : {I : Type ℓ'} (ψ : CommAlgebraHom A B)
+             (f : CommAlgebraHom (R [ I ]) A)
+             → (fst ψ) ∘ evaluateAt A f ≡ evaluateAt B (ψ ∘a f)
+  naturalEvR ψ f = refl
 
-  {-
+  {-
     Hom(R[I],A) ← (I → A)
          ↓          ↓ψ
     Hom(R[I],B) ← (I → B)
   -}
-  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 ψ ∘ ϕ))     ∎)
-
-  {-
+  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
-
-module _ {R : CommRing ℓ} where
-  {-
+  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
+
+module _ {R : CommRing ℓ} where
+  {-
     Prove that the FreeCommAlgebra over R on zero generators is
     isomorphic to the initial R-Algebra - R itsself.
   -}
-  freeOn⊥ : CommAlgebraEquiv (R [ ⊥ ]) (initialCAlg R)
-  freeOn⊥ =
-     equivByInitiality
-        R (R [ ⊥ ])
-          {- Show that R[⊥] has the universal property of the
+  freeOn⊥ : CommAlgebraEquiv (R [ ⊥ ]) (initialCAlg R)
+  freeOn⊥ =
+     equivByInitiality
+        R (R [ ⊥ ])
+          {- Show that R[⊥] has the universal property of the
              initial R-Algbera and conclude that those are isomorphic -}
-        λ B →  let to : CommAlgebraHom (R [ ⊥ ]) B → (⊥ → fst B)
-                   to = evaluateAt B
-
-                   from :  (⊥ → fst B) → CommAlgebraHom (R [ ⊥ ]) B
-                   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)
-
-                   equiv : CommAlgebraHom (R [ ⊥ ]) B ≃ (⊥ → fst B)
-                   equiv =
-                     isoToEquiv
-                       (iso to from (λ x → isContr→isOfHLevel 1 isContr⊥→A _ _) from-to)
-               in isOfHLevelRespectEquiv 0 (invEquiv equiv) isContr⊥→A
-
-module _ {R : CommRing ℓ} {I : Type ℓ} where
-  baseRingHom : CommRingHom R (CommAlgebra→CommRing (R [ I ]))
-  baseRingHom = snd (Iso.fun (CommAlgChar.CommAlgIso R) (R [ I ]))
+        λ B →  let to : CommAlgebraHom (R [ ⊥ ]) B → (⊥ → fst B)
+                   to = evaluateAt B
+
+                   from :  (⊥ → fst B) → CommAlgebraHom (R [ ⊥ ]) B
+                   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)
+
+                   equiv : CommAlgebraHom (R [ ⊥ ]) B ≃ (⊥ → fst B)
+                   equiv =
+                     isoToEquiv
+                       (iso to from (λ x → isContr→isOfHLevel 1 isContr⊥→A _ _) from-to)
+               in isOfHLevelRespectEquiv 0 (invEquiv equiv) isContr⊥→A
+
+module _ {R : CommRing ℓ} {I : Type ℓ} where
+  baseRingHom : CommRingHom R (CommAlgebra→CommRing (R [ I ]))
+  baseRingHom = snd (Iso.fun (CommAlgChar.CommAlgIso R) (R [ I ]))
\ No newline at end of file diff --git a/Cubical.Algebra.Polynomials.TypevariateHIT.EquivUnivariateListPoly.html b/Cubical.Algebra.Polynomials.TypevariateHIT.EquivUnivariateListPoly.html index cdc5e85d02..11634fda24 100644 --- a/Cubical.Algebra.Polynomials.TypevariateHIT.EquivUnivariateListPoly.html +++ b/Cubical.Algebra.Polynomials.TypevariateHIT.EquivUnivariateListPoly.html @@ -13,8 +13,8 @@ open import Cubical.Algebra.Algebra open import Cubical.Algebra.CommAlgebra open import Cubical.Algebra.Polynomials.TypevariateHIT - renaming (inducedHomUnique to inducedHomUniqueHIT; - isIdByUMP to isIdByUMP-HIT) + renaming (inducedHomUnique to inducedHomUniqueHIT; + isIdByUMP to isIdByUMP-HIT) open import Cubical.Algebra.Polynomials.UnivariateList.UniversalProperty renaming (generator to generatorList; inducedHom to inducedHomList; @@ -25,12 +25,12 @@ ℓ : Level module _ {R : CommRing ℓ} where - open Theory renaming (inducedHom to inducedHomHIT) + open Theory renaming (inducedHom to inducedHomHIT) open CommRingStr ⦃...⦄ private instance _ = snd R - X-HIT = Construction.var {R = R} {I = Unit} tt + X-HIT = Construction.var {R = R} {I = Unit} tt X-List = generatorList R {- @@ -40,34 +40,34 @@ private open AlgebraHoms open Iso - to : CommAlgebraHom (R [ Unit ]) (ListPolyCommAlgebra R) + to : CommAlgebraHom (R [ Unit ]) (ListPolyCommAlgebra R) to = inducedHomHIT (ListPolyCommAlgebra R) (λ _ → X-List) - from : CommAlgebraHom (ListPolyCommAlgebra R) (R [ Unit ]) - from = inducedHomList R (CommAlgebra→Algebra (R [ Unit ])) X-HIT + from : CommAlgebraHom (ListPolyCommAlgebra R) (R [ Unit ]) + from = inducedHomList R (CommAlgebra→Algebra (R [ Unit ])) X-HIT toPresX : fst to X-HIT ≡ X-List toPresX = refl fromPresX : fst from X-List ≡ X-HIT - fromPresX = inducedMapGenerator R (CommAlgebra→Algebra (R [ Unit ])) X-HIT + fromPresX = inducedMapGenerator R (CommAlgebra→Algebra (R [ Unit ])) X-HIT idList = AlgebraHoms.idAlgebraHom (CommAlgebra→Algebra (ListPolyCommAlgebra R)) - idHIT = AlgebraHoms.idAlgebraHom (CommAlgebra→Algebra (R [ Unit ])) + idHIT = AlgebraHoms.idAlgebraHom (CommAlgebra→Algebra (R [ Unit ])) toFrom : (x : ⟨ ListPolyCommAlgebra R ⟩) → fst to (fst from x) ≡ x toFrom = isIdByUMP-List R (to ∘a from) (cong (fst to) fromPresX) - fromTo : (x : ⟨ R [ Unit ] ⟩) → fst from (fst to x) ≡ x + fromTo : (x : ⟨ R [ Unit ] ⟩) → fst from (fst to x) ≡ x fromTo = isIdByUMP-HIT (from ∘a to) λ {tt → fromPresX} - typevariateListPolyIso : Iso ⟨ R [ Unit ] ⟩ ⟨ ListPolyCommAlgebra R ⟩ + typevariateListPolyIso : Iso ⟨ R [ Unit ] ⟩ ⟨ ListPolyCommAlgebra R ⟩ fun typevariateListPolyIso = fst to inv typevariateListPolyIso = fst from rightInv typevariateListPolyIso = toFrom leftInv typevariateListPolyIso = fromTo - typevariateListPolyEquiv : CommAlgebraEquiv (R [ Unit ]) (ListPolyCommAlgebra R) + typevariateListPolyEquiv : CommAlgebraEquiv (R [ Unit ]) (ListPolyCommAlgebra R) fst typevariateListPolyEquiv = isoToEquiv typevariateListPolyIso snd typevariateListPolyEquiv = snd to