    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Homomorphism proofs for variables and constants over polynomials
    ------------------------------------------------------------------------

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

    open import Tactic.RingSolver.Core.Polynomial.Parameters

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

    open import Data.Product.Base    using (_,_)
    open import Data.Vec.Base as Vec using (Vec)
    open import Data.Fin.Base        using (Fin)
    open import Data.List.Kleene

    open Homomorphism homo

    open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas homo
    open import Tactic.RingSolver.Core.Polynomial.Base (Homomorphism.from homo)
    open import Tactic.RingSolver.Core.Polynomial.Reasoning (Homomorphism.to homo)
    open import Tactic.RingSolver.Core.Polynomial.Semantics homo

    ι-hom : ∀ {n} (i : Fin n) (Ρ : Vec Carrier n) → ⟦ ι i ⟧ Ρ ≈ Vec.lookup Ρ i
    ι-hom i Ρ′ = let (ρ , Ρ) = drop-1 (space≤′n i) Ρ′ in begin
      ⟦ (κ Raw.1# Δ 1 ∷↓ []) ⊐↓ space≤′n i ⟧ Ρ′  ≈⟨ ⊐↓-hom (κ Raw.1# Δ 1 ∷↓ []) (space≤′n i) Ρ′ ⟩
      ⅀?⟦ κ Raw.1# Δ 1 ∷↓ [] ⟧ (ρ , Ρ)           ≈⟨ ∷↓-hom-s (κ Raw.1#) 0 [] ρ Ρ  ⟩
      ρ * ⟦ κ Raw.1# ⟧ Ρ                         ≈⟨ *≫ 1-homo ⟩
      ρ * 1#                                     ≈⟨ *-identityʳ ρ ⟩
      ρ                                          ≡⟨ drop-1⇒lookup i Ρ′ ⟩
      Vec.lookup Ρ′ i                            ∎