#### 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 Overture using (π ; π₯ ; Signature)

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

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

open import Relation.Binary.PropositionalEquality as β‘ using ( _β‘_ )

import Relation.Binary.Reasoning.Setoid as SetoidReasoning

-- Imports from Agda Universal Algebra Library -----------------------------------
open  import Overture                         using ( β£_β£ ; β₯_β₯ )
open  import Base.Terms               {π = π} using ( Term )
open  import Setoid.Algebras          {π = π} using ( Algebra ; _Μ_ ; ov ; β¨ )
open  import Setoid.Homomorphisms     {π = π} using ( hom ; IsHom )
open  import Setoid.Terms.Properties  {π = π} using ( free-lift )
open  import Setoid.Terms.Basic       {π = π}
using ( module Environment ; π» ; _β_ ; β-isRefl )

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 Environment π¨  using () renaming ( β¦_β§ to β¦_β§β )
open Environment π©  using () renaming ( β¦_β§ to β¦_β§β )
open SetoidReasoning B
open IsHom

private
hfunc = β£ hh β£

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.

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

```

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 )
```