------------------------------------------------------------------------
-- The Agda standard library
--
-- Some specialised instances of the ring solver
------------------------------------------------------------------------

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

open import Tactic.RingSolver.Core.Polynomial.Parameters

-- Here, we provide proofs of homomorphism between the operations
-- defined on polynomials and those on the underlying ring.

module Tactic.RingSolver.Core.Polynomial.Homomorphism
  {r₁ r₂ r₃ r₄}
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where

-- Proofs for each component of the polynomial
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition       homo using (⊞-hom) public
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Multiplication homo using (⊠-hom) public
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation       homo using (⊟-hom) public
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Exponentiation homo using (⊡-hom) public
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Constants      homo using (κ-hom) public
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Variables      homo using (ι-hom) public