{-# OPTIONS --cubical-compatible --safe #-}
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
record RawCoeff ℓ₁ ℓ₂ : Set (suc (ℓ₁ ⊔ ℓ₂)) where
field
rawRing : RawRing ℓ₁ ℓ₂
isZero : RawRing.Carrier rawRing → Bool
open RawRing rawRing public
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 ⟧ᵣ