{-# OPTIONS --cubical-compatible --safe #-}
open import Tactic.RingSolver.Core.Polynomial.Parameters
module Tactic.RingSolver.Core.Polynomial.Homomorphism.Constants
{r₁ r₂ r₃ r₄}
(homo : Homomorphism r₁ r₂ r₃ r₄)
where
open Homomorphism homo
open import Data.Vec.Base using (Vec)
open import Tactic.RingSolver.Core.Polynomial.Base (Homomorphism.from homo)
open import Tactic.RingSolver.Core.Polynomial.Semantics homo
κ-hom : ∀ {n} (x : Raw.Carrier) (Ρ : Vec Carrier n) → ⟦ κ x ⟧ Ρ ≈ ⟦ x ⟧ᵣ
κ-hom x _ = refl