    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Bundles of parameters for passing to the Ring Solver
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    -- This module packages up all the stuff that's passed to the other
    -- modules in a convenient form.

    module Tactic.RingSolver.Core.Polynomial.Parameters where

    open import Algebra.Bundles using (RawRing)
    open import Data.Bool.Base using (Bool; T)
    open import Level
    open import Relation.Unary
    open import Tactic.RingSolver.Core.AlmostCommutativeRing

    -- This record stores all the stuff we need for the coefficients:
    --
    --  * A raw ring
    --  * A (decidable) predicate on "zeroeness"
    --
    -- It's used for defining the operations on the Horner normal form.
    record RawCoeff ℓ₁ ℓ₂ : Set (suc (ℓ₁ ⊔ ℓ₂)) where
      field
        rawRing : RawRing ℓ₁ ℓ₂
        isZero  : RawRing.Carrier rawRing → Bool

      open RawRing rawRing public

    -- This record stores the full information we need for converting
    -- to the final ring.
    record Homomorphism ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Set (suc (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)) where
      field
        from : RawCoeff ℓ₁ ℓ₂
        to   : AlmostCommutativeRing ℓ₃ ℓ₄

      module Raw = RawCoeff from
      open AlmostCommutativeRing to public

      field
        morphism : Raw.rawRing -Raw-AlmostCommutative⟶ to
      open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧ᵣ) public
      field
        Zero-C⟶Zero-R : ∀ x → T (Raw.isZero x) → 0# ≈  ⟦ x ⟧ᵣ