(σ : Type v) →
  (R A : CommRingCat) →
    [inst : TopologicalSpace ↑R] →
      [IsTopologicalRing ↑R] →
        ({ carrier := MvPolynomial σ ↑A, commRing := MvPolynomial.instCommRingMvPolynomial } ⟶ R) ≃ₜ (A ⟶ R) × (σ → ↑R)