#### Term Operations for Setoid Algebras

This section presents the Setoid.Terms.Operations module of the Agda Universal Algebra Library.

Here we define term operations which are simply terms interpreted in a particular algebra, and we prove some compatibility properties of term operations.

```{-# OPTIONS --without-K --exact-split --safe #-}

open import Base.Algebras.Basic using ( π ; π₯ ; Signature )

module Setoid.Terms.Operations {π : Signature π π₯} where

-- Imports from Agda and the Agda Standard Library ---------------------
open import Agda.Primitive    using ( Level )  renaming ( Set to Type )
open import Data.Product      using ( _,_ )
open import Function.Base     using ( _β_ )
open import Function.Bundles  using ()         renaming ( Func to _βΆ_ )
open import Relation.Binary   using ( Setoid )
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Relation.Binary.PropositionalEquality as β‘ using ( _β‘_ )

-- Imports from Agda Universal Algebra Library ----------------------------------------------
open import Base.Overture.Preliminaries          using ( β£_β£ ; β₯_β₯ )
open import Base.Terms.Basic            {π = π}  using ( Term )

open import Setoid.Algebras.Basic       {π = π}  using ( Algebra ; _Μ_ ; ov )
open import Setoid.Algebras.Products    {π = π}  using ( β¨ )
open import Setoid.Homomorphisms.Basic  {π = π}  using ( hom ; IsHom )
open import Setoid.Terms.Basic          {π = π}  using ( module Environment ; π» ; _β_ ; β-isRefl )
open import Setoid.Terms.Properties     {π = π}  using ( free-lift )

open Term
open _βΆ_ using ( cong ) renaming ( f to _β¨\$β©_ )

private variable
Ξ± Οα΅ Ξ² Οα΅ Ο Ο ΞΉ : Level
X : Type Ο

```

It turns out that the intepretation of a term is the same as the `free-lift` (modulo argument order and assuming function extensionality).

```module _ {π¨ : Algebra Ξ± Οα΅} where
open Algebra π¨ using ( Interp ) renaming (Domain to A )
open Setoid A using ( _β_ ; refl ) renaming ( Carrier to β£Aβ£ )
open Environment π¨ using ( β¦_β§ )

free-lift-interp : (Ξ· : X β β£Aβ£)(p : Term X)
β                 β¦ p β§ β¨\$β© Ξ· β (free-lift{π¨ = π¨} Ξ·) p

free-lift-interp Ξ· (β x) = refl
free-lift-interp Ξ· (node f t) = cong Interp (β‘.refl , (free-lift-interp Ξ·) β t)

module _ {X : Type Ο} where
open Algebra (π» X) using ( Interp ) renaming (Domain to TX )
open Setoid TX using ( _β_ ; refl ) renaming ( Carrier to β£TXβ£ )
open Environment (π» X) using ( β¦_β§ ; ββEqual )
open SetoidReasoning TX

term-interp : (f : β£ π β£){s t : β₯ π β₯ f β Term X} β (β i β s i β t i)
β            β Ξ· β β¦ node f s β§ β¨\$β© Ξ· β β¦ node f t β§ β¨\$β© Ξ· -- (f Μ π» X) t
term-interp f {s}{t} st Ξ· = cong Interp (β‘.refl , Ξ» i β ββEqual (s i) (t i) (st i) Ξ· )

term-agreement : (p : Term X) β p β β¦ p β§ β¨\$β© β
term-agreement (β x) = refl
term-agreement (node f t) = cong Interp (β‘.refl , (Ξ» i β term-agreement (t i)))

```

#### Interpretation of terms in product algebras

```module _ {X : Type Ο }{I : Type ΞΉ}
(π : I β Algebra Ξ± Οα΅) where
open Algebra (β¨ π) using (Interp) renaming ( Domain to β¨A )
open Setoid β¨A using ( _β_ ; refl )
open Environment (β¨ π) using () renaming ( β¦_β§ to β¦_β§β )
open Environment using ( β¦_β§ ; ββEqual )

interp-prod : (p : Term X)
β            β Ο β β¦ p β§β β¨\$β© Ο β (Ξ» i β (β¦ π i β§ p) β¨\$β© (Ξ» x β (Ο x) i))
interp-prod (β x) = Ξ» Ο i β ββEqual (π i) (β x) (β x) β-isRefl Ξ» x' β (Ο x) i
interp-prod (node f t) = Ξ» Ο i β cong Interp (β‘.refl , (Ξ» j k β interp-prod (t j) Ο k)) i

```

#### Compatibility of terms

We now prove two important facts about term operations. The first of these, which is used very often in the sequel, asserts that every term commutes with every homomorphism.

```module _ {π¨ : Algebra Ξ± Οα΅}{π© : Algebra Ξ² Οα΅}(hh : hom π¨ π©) where
open Algebra π¨ using () renaming (Domain to A ; Interp to Interpβ )
open Setoid A using () renaming ( _β_ to _ββ_ ; Carrier to β£Aβ£ )

open Algebra π© using () renaming (Domain to B ; Interp to Interpβ )
open Setoid B using ( _β_ ; sym ; refl )

open SetoidReasoning B

private
hfunc = β£ hh β£

open Environment π¨ using ( ) renaming ( β¦_β§ to β¦_β§β )
open Environment π© using ( ) renaming ( β¦_β§ to β¦_β§β )
open IsHom
comm-hom-term : (t : Term X) (a : X β β£Aβ£)
-----------------------------------------
β             h (β¦ t β§β β¨\$β© a) β β¦ t β§β β¨\$β© (h β a)

comm-hom-term (β x) a = refl
comm-hom-term (node f t) a = goal
where
goal : h (β¦ node f t β§β β¨\$β© a) β (β¦ node f t β§β β¨\$β© (h β a))
goal =
begin
h (β¦ node f t β§β β¨\$β© a)             ββ¨ (compatible β₯ hh β₯) β©
(f Μ π©)(Ξ» i β h (β¦ t i β§β β¨\$β© a))   ββ¨ cong Interpβ (β‘.refl , Ξ» i β comm-hom-term (t i) a) β©
(β¦ node f t β§β β¨\$β© (h β a))
β

```

#### Substitution

A substitution from `Y` to `X` is simply a function from `Y` to `X`, and the application of a substitution is represented as follows.

```_[_] : {Ο : Level}{X Y : Type Ο} β Term Y β (Y β X) β Term X
(β y) [ Ο ] = β (Ο y)
(node f t)  [ Ο ] = node f Ξ» i β t i [ Ο ]

```

Alternatively, we may want a substitution that replaces each variable symbol in `Y`, not with an element of `X`, but with a term from `Term X`.

```-- Substerm X Y, an inhabitant of which replaces each variable symbol in Y with a term from Term X.
Substerm : (X Y : Type Ο) β Type (ov Ο)
Substerm X Y = (y : Y) β Term X

-- Application of a Substerm.
_[_]t : {X Y : Type Ο } β Term Y β Substerm X Y β Term X
(β y) [ Ο ]t = Ο y
(node f t) [ Ο ]t = node f (Ξ» z β (t z) [ Ο ]t )

```