{-# OPTIONS --safe --lossy-unification #-}
module Cubical.Algebra.GradedRing.Instances.PolynomialsFun where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty as 
open import Cubical.Data.Nat hiding (_·_) renaming (_+_ to _+n_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Ring
open import Cubical.Algebra.GradedRing.Base
open import Cubical.Algebra.GradedRing.DirectSumFun

private variable
   : Level

module _
  (ARing@(A , Astr) : Ring )
  (n : )
  where

  open RingStr Astr
  open RingTheory ARing

  PolyGradedRing : GradedRing ℓ-zero 
  PolyGradedRing = ⊕Fun-GradedRing
                   _+n_ (makeIsMonoid isSetℕ +-assoc +-zero λ _  refl)  _ _  refl)
                    _  A)
                    _  snd (Ring→AbGroup ARing))
                   1r _·_ 0LeftAnnihilates 0RightAnnihilates
                    a b c  ΣPathP ((+-assoc _ _ _) , (·Assoc _ _ _)))
                    a  ΣPathP ((+-zero _) , (·IdR _)))
                    a  ΣPathP (refl , (·IdL _)))
                   ·DistR+
                   ·DistL+