Typevariate and list-based polynomials are isomorphic

Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda

@@ -352,17 +352,17 @@ Iso.leftInv (homMapIso {R = R} {I = I} A) =
   λ f → Σ≡Prop (λ f → isPropIsCommAlgebraHom {M = R [ I ]} {N = A} f)
                (Theory.homRetrievable A f)
 
-homMapPath : {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R (ℓ-max ℓ ℓ'))
-             → CommAlgebraHom (R [ I ]) A ≡ (I → fst A)
-homMapPath A = isoToPath (homMapIso A)
-
 inducedHomUnique :
   {R : CommRing ℓ} {I : Type ℓ'} (A : CommAlgebra R ℓ'') (φ : I → fst A )
   → (f : CommAlgebraHom (R [ I ]) A) → ((i : I) → fst f (Construction.var i) ≡ φ i)
   → f ≡ 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 ℓ'')

Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda

@@ -37,24 +37,27 @@ module _ (R : CommRing ℓ) where
             (ListPoly ,
              constantPolynomialHom R)
 
+  private
+    X : ⟨ ListPolyCommAlgebra ⟩
+    X = 0r ∷ 1r ∷ []
+
+  {- export the generator 'X' -}
+  generator = X
+
   {- Universal Property -}
   module _ (A : Algebra (CommRing→Ring R) ℓ') where
     open AlgebraStr ⦃...⦄ using (_⋆_; 0a; 1a; ⋆IdL; ⋆DistL+; ⋆DistR+; ⋆AssocL; ⋆AssocR; ⋆Assoc)
     private instance
       _ = snd A
       _ = snd (Algebra→Ring A)
       _ = snd (CommAlgebra→Algebra ListPolyCommAlgebra)
-    private
-      X : ⟨ ListPolyCommAlgebra ⟩
-      X = 0r ∷ 1r ∷ []
 
     module _ (x : ⟨ A ⟩) where
       open AlgebraTheory using (⋆AnnihilL; ⋆AnnihilR)
       open RingTheory using (0RightAnnihilates; 0LeftAnnihilates)
       open AbGroupTheory using (comm-4)
       open PolyMod using (ElimProp; elimProp2; isSetPoly)
 
-
       inducedMap : ⟨ ListPolyCommAlgebra ⟩ → ⟨ A ⟩
       inducedMap [] = 0a
       inducedMap (a ∷ p) = a ⋆ 1a + (x · inducedMap p)
@@ -216,10 +219,31 @@ module _ (R : CommRing ℓ) where
             useSolver : (r : ⟨ R ⟩) → r ≡ (r · 1r) + 0r
             useSolver = solve R
 
+
     {- Reforumlation in terms of the R-AlgebraHom from R[X] to A -}
     indcuedHomEquivalence : AlgebraHom (CommAlgebra→Algebra ListPolyCommAlgebra) A ≃ ⟨ A ⟩
     fst indcuedHomEquivalence f = fst f X
     fst (fst (equiv-proof (snd indcuedHomEquivalence) x)) = inducedHom x
     snd (fst (equiv-proof (snd indcuedHomEquivalence) x)) = inducedMapGenerator x
     snd (equiv-proof (snd indcuedHomEquivalence) x) (g , gX≡x) =
       Σ≡Prop (λ _ → isSetAlgebra A _ _) (sym (inducedHomUnique x g gX≡x))
+
+    equalByUMP : (f g : AlgebraHom (CommAlgebra→Algebra ListPolyCommAlgebra) A)
+                 → fst f X ≡ fst g X
+                 → (x : ⟨ ListPolyCommAlgebra ⟩) → fst f x ≡ fst g x
+    equalByUMP f g fX≡gX x =
+      fst f x                      ≡[ i ]⟨ fst (inducedHomUnique (fst f X) f refl i) x  ⟩
+      fst (inducedHom (fst f X)) x ≡[ i ]⟨ fst (inducedHom (fX≡gX i)) x ⟩
+      fst (inducedHom (fst g X)) x ≡[ i ]⟨ fst (inducedHomUnique (fst g X) g refl (~ i)) x ⟩
+      fst g x ∎
+
+  {- A corollary, which is useful for constructing isomorphisms to
+     algebras with the same universal property -}
+  isIdByUMP : (f : CommAlgebraHom ListPolyCommAlgebra ListPolyCommAlgebra)
+              → fst f X ≡ X
+              → (x : ⟨ ListPolyCommAlgebra ⟩) → fst f x ≡ x
+  isIdByUMP f =
+    equalByUMP (CommAlgebra→Algebra ListPolyCommAlgebra)
+               f
+               (idAlgebraHom (CommAlgebra→Algebra ListPolyCommAlgebra))
+    where open AlgebraHoms using (idAlgebraHom)

Cubical/Algebra/Polynomials/TypevariateHIT.agda

@@ -0,0 +1,4 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.Polynomials.TypevariateHIT where
+
+open import Cubical.Algebra.Polynomials.TypevariateHIT.Base public

Cubical/Algebra/Polynomials/TypevariateHIT/EquivUnivariateListPoly.agda

@@ -0,0 +1,75 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.Polynomials.TypevariateHIT.EquivUnivariateListPoly where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Structure
+
+open import Cubical.Data.Unit
+
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.Algebra
+open import Cubical.Algebra.CommAlgebra
+open import Cubical.Algebra.Polynomials.TypevariateHIT
+            renaming (inducedHomUnique to inducedHomUniqueHIT;
+                      isIdByUMP to isIdByUMP-HIT)
+open import Cubical.Algebra.Polynomials.UnivariateList.UniversalProperty
+            renaming (generator to generatorList;
+                      inducedHom to inducedHomList;
+                      inducedHomUnique to inducedHomUniqueList;
+                      isIdByUMP to isIdByUMP-List)
+
+private variable
+  ℓ : Level
+
+module _ {R : CommRing ℓ} where
+  open Theory renaming (inducedHom to inducedHomHIT)
+  open CommRingStr ⦃...⦄
+  private
+    instance
+      _ = snd R
+    X-HIT = Construction.var {R = R} {I = Unit} tt
+    X-List = generatorList R
+
+  {-
+    Construct an iso between the two versions of polynomials.
+    Just using the universal properties to manually show that the two algebras are isomorphic
+  -}
+  private
+    open AlgebraHoms
+    open Iso
+    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
+
+    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
+
+    idList = AlgebraHoms.idAlgebraHom (CommAlgebra→Algebra (ListPolyCommAlgebra R))
+    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 = isIdByUMP-HIT (from ∘a to) λ {tt → fromPresX}
+
+  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)
+  fst typevariateListPolyEquiv = isoToEquiv typevariateListPolyIso
+  snd typevariateListPolyEquiv = snd to
+
+  typevariateListPolyGenerator :
+    fst (fst typevariateListPolyEquiv) X-HIT ≡ X-List
+  typevariateListPolyGenerator = refl