start with OnCoproduct, change default notation for R[I]

Cubical/Algebra/CommAlgebraAlt/Instances/Polynomials.agda

@@ -9,11 +9,10 @@ open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate
 
 private
   variable
-    ℓ ℓ' : Level
-
-_[_] : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R _
-R [ I ] = (R [ I ]ᵣ) , constPolynomial R I
+    ℓ ℓ' ℓ'' : Level
 
+_[_]ₐ : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R _
+R [ I ]ₐ = (R [ I ]) , constPolynomial R I
 
 {-
 evaluateAt : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'')

Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Base.agda

@@ -81,15 +81,15 @@ module Construction (R : CommRing ℓ) where
     constIsCommRingHom : (I : Type ℓ') → IsCommRingHom (R .snd) (const {I = I}) (commRingStr I)
     constIsCommRingHom I = makeIsCommRingHom refl +HomConst ·HomConst
 
-_[_]ᵣ : (R : CommRing ℓ) (I : Type ℓ') → CommRing (ℓ-max ℓ ℓ')
-fst (R [ I ]ᵣ) = Construction.R[_] R I
-snd (R [ I ]ᵣ) = Construction.commRingStr R I
+_[_] : (R : CommRing ℓ) (I : Type ℓ') → CommRing (ℓ-max ℓ ℓ')
+fst (R [ I ]) = Construction.R[_] R I
+snd (R [ I ]) = Construction.commRingStr R I
 
-constPolynomial : (R : CommRing ℓ) (I : Type ℓ') → CommRingHom R (R [ I ]ᵣ)
+constPolynomial : (R : CommRing ℓ) (I : Type ℓ') → CommRingHom R (R [ I ])
 constPolynomial R I .fst = let open Construction R
                            in R[_].const
 constPolynomial R I .snd = Construction.constIsCommRingHom R I
 
 opaque
-  var : {R : CommRing ℓ} {I : Type ℓ'} → I → ⟨ R [ I ]ᵣ ⟩
+  var : {R : CommRing ℓ} {I : Type ℓ'} → I → ⟨ R [ I ] ⟩
   var = Construction.var

Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/OnCoproduct.agda

@@ -0,0 +1,81 @@
+{-# OPTIONS --safe #-}
+{-
+ The goal of this module is to show that for two types I,J, there is an
+ isomorphism of algebras
+
+    R[I][J] ≃ R[ I ⊎ J ]
+
+  where '⊎' is the disjoint sum.
+-}
+module Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate.OnCoproduct where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function using (_∘_)
+open import Cubical.Foundations.Structure using (⟨_⟩)
+
+open import Cubical.Data.Sum as ⊎
+open import Cubical.Data.Sigma
+
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommRing.Instances.Polynomials.Typevariate
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module CalculatePolynomialsOnCoproduct (R : CommRing ℓ) (I J : Type ℓ) where
+  private
+    I→I+J : CommRingHom (R [ I ]) (R [ I ⊎ J ])
+    I→I+J = inducedHom (R [ I ⊎ J ]) (constPolynomial R (I ⊎ J)) (var ∘ inl)
+
+    to : CommRingHom ((R [ I ]) [ J ]) (R [ I ⊎ J ])
+    to = inducedHom (R [ I ⊎ J ]) I→I+J (var ∘ inr)
+
+    constPolynomialIJ : CommRingHom R ((R [ I ]) [ J ])
+    constPolynomialIJ = constPolynomial _ _ ∘cr constPolynomial _ _
+
+    evalVarTo : to .fst ∘ var ≡ var ∘ inr
+    evalVarTo = evalInduce (R [ I ⊎ J ]) I→I+J (var ∘ inr)
+
+    commConstTo : to ∘cr constPolynomialIJ ≡ constPolynomial _ _
+    commConstTo = CommRingHom≡ refl
+
+    mapVars : I ⊎ J → ⟨ (R [ I ]) [ J ] ⟩
+    mapVars (inl i) = constPolynomial _ _ $cr var i
+    mapVars (inr j) = var j
+
+    to∘MapVars : to .fst ∘ mapVars ≡ var
+    to∘MapVars = funExt λ {(inl i) → to .fst (constPolynomial _ _ $cr var i)
+                                         ≡⟨ cong (λ z → z i) (evalInduce (R [ I ⊎ J ]) (constPolynomial R (I ⊎ J)) (var ∘ inl)) ⟩
+                                     var (inl i) ∎;
+                           (inr j) → (to .fst (var j) ≡⟨ cong (λ z → z j) evalVarTo ⟩ var (inr j) ∎)}
+
+    from : CommRingHom (R [ I ⊎ J ]) ((R [ I ]) [ J ])
+    from = inducedHom
+               ((R [ I ]) [ J ])
+               (constPolynomial (R [ I ]) J ∘cr constPolynomial R I)
+               mapVars
+
+    evalVarFrom : from .fst ∘ var ≡ mapVars
+    evalVarFrom = evalInduce ((R [ I ]) [ J ]) (constPolynomial (R [ I ]) J ∘cr constPolynomial R I) mapVars
+
+    toFrom : to ∘cr from ≡ (idCommRingHom _)
+    toFrom =
+      idByIdOnVars
+        (to ∘cr from)
+        (to .fst ∘ from .fst ∘ constPolynomial R (I ⊎ J) .fst  ≡⟨⟩
+         constPolynomial R (I ⊎ J) .fst ∎)
+        (to .fst ∘ from .fst ∘ var       ≡⟨ cong (to .fst ∘_) evalVarFrom ⟩
+         to .fst ∘ mapVars               ≡⟨ to∘MapVars ⟩
+         var ∎)
+{-
+    fromTo : from ∘cr to ≡ (idCommRingHom _)
+    fromTo =
+      idByIdOnVars
+        (from ∘cr to)
+        (from .fst ∘ to .fst ∘ constPolynomial (R [ I ]) J .fst ≡⟨⟩
+         from .fst ∘ I→I+J .fst
+           ≡⟨ cong fst (hom≡ByValuesOnVars ((R [ I ]) [ J ]) {!from ∘cr I→I+J!} {!I→I+J!} {!!} {!!} {!!} {!!}) ⟩
+         constPolynomial (R [ I ]) J .fst ∎)
+        (from .fst ∘ to .fst ∘ var ≡⟨ {!!} ⟩ var ∎)
+-}

Cubical/Algebra/CommRing/Instances/Polynomials/Typevariate/Properties.agda

@@ -35,7 +35,7 @@ module _ {R : CommRing ℓ} {I : Type ℓ'} where
   open CommRingStr ⦃...⦄
   private instance
     _ = snd R
-    _ = snd (R [ I ]ᵣ)
+    _ = snd (R [ I ])
 
   module C = Construction
   open C using (const)
@@ -44,29 +44,29 @@ module _ {R : CommRing ℓ} {I : Type ℓ'} where
     Construction of the 'elimProp' eliminator.
   -}
   module _
-    {P : ⟨ R [ I ]ᵣ ⟩ → Type ℓ''}
+    {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))
+    (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 : ⟨ 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)
+                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 ]ᵣ ⟩} →
+        {x0 x1 : ⟨ R [ I ] ⟩} →
         (p : x0 ≡ x1) →
         (Px0 : P (x0)) →
         (Px1 : P (x1)) →
@@ -160,7 +160,7 @@ module _ {R : CommRing ℓ} {I : Type ℓ'} where
 
     open IsCommRingHom
 
-    inducedMap : ⟨ R [ I ]ᵣ ⟩ → ⟨ S ⟩
+    inducedMap : ⟨ R [ I ] ⟩ → ⟨ S ⟩
     inducedMap (C.var x) = φ x
     inducedMap (const r) = (f .fst r)
     inducedMap (P C.+ Q) = (inducedMap P) + (inducedMap Q)
@@ -198,7 +198,7 @@ module _ {R : CommRing ℓ} {I : Type ℓ'} where
     module _ where
       open IsCommRingHom
 
-      inducedHom : CommRingHom (R [ I ]ᵣ) S
+      inducedHom : CommRingHom (R [ I ]) S
       inducedHom .fst = inducedMap
       inducedHom .snd .pres0 = pres0 (f .snd)
       inducedHom .snd .pres1 = pres1 (f. snd)
@@ -214,11 +214,11 @@ module _  {R : CommRing ℓ} {I : Type ℓ'} (S : CommRing ℓ'') (f : CommRingH
   open CommRingStr ⦃...⦄
   private instance
     _ = S .snd
-    _ = (R [ I ]ᵣ) .snd
+    _ = (R [ I ]) .snd
   open IsCommRingHom
 
-  evalVar : CommRingHom (R [ I ]ᵣ) S → I → ⟨ S ⟩
-  evalVar f = f .fst ∘ var
+  evalVar : CommRingHom (R [ I ]) S → I → ⟨ S ⟩
+  evalVar h = h .fst ∘ var
 
   opaque
     unfolding var
@@ -228,11 +228,11 @@ module _  {R : CommRing ℓ} {I : Type ℓ'} (S : CommRing ℓ'') (f : CommRingH
 
   opaque
     unfolding var
-    induceEval : (g : CommRingHom (R [ I ]ᵣ) S)
+    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 ⟩
+      let theMap : ⟨ R [ I ] ⟩ → ⟨ S ⟩
           theMap = inducedMap S f (evalVar g)
       in
       CommRingHom≡ $
@@ -254,8 +254,26 @@ module _  {R : CommRing ℓ} {I : Type ℓ'} (S : CommRing ℓ'') (f : CommRingH
 
   opaque
     inducedHomUnique : (φ : I → ⟨ S ⟩)
-                 (g : CommRingHom (R [ 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