---
layout: default
title : "Setoid.Terms.Operations module (The Agda Universal Algebra Library)"
date : "2021-09-25"
author: "agda-algebras development team"
---

#### 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.


<!--
```agda
{-# OPTIONS --cubical-compatible --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 ( proj₁ ; projβ‚‚ ; OperationSymbolsOf ; ArityOf )
open  import Overture.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 ( to 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).


```agda
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 )
  open Environment (𝑻 X)  using ( ⟦_⟧ ; ≐→Equal )
  open SetoidReasoning TX

  term-interp :  (f : OperationSymbolsOf 𝑆){s t : ArityOf 𝑆 f β†’ Term X} β†’ (βˆ€ i β†’ s i ≐ t i)
   β†’ βˆ€ Ξ· β†’ ⟦ node f s ⟧ ⟨$⟩ Ξ· β‰ˆ ⟦ node f 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

```agda
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.

```agda
module _ {𝑨 : Algebra Ξ± ρᡃ}{𝑩 : Algebra Ξ² ρᡇ}(hh : hom 𝑨 𝑩) where
  open Algebra 𝑨      using () renaming (Domain to A )
  open Setoid A       using () renaming ( Carrier to ∣A∣ )
  open Algebra 𝑩      using () renaming (Domain to B ; Interp to Interpβ‚‚ )
  open Setoid B       using ( _β‰ˆ_ ; refl )
  open Environment 𝑨  using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚ )
  open Environment 𝑩  using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚‚ )
  open SetoidReasoning B
  open IsHom

  private
    h : A ⟢ B
    h = proj₁ hh

  comm-hom-term :
    (t : Term X) (a : X β†’ ∣A∣) β†’ h ⟨$⟩ (⟦ t βŸ§β‚ ⟨$⟩ a) β‰ˆ ⟦ t βŸ§β‚‚ ⟨$⟩ Ξ» i β†’ h ⟨$⟩ a i

  comm-hom-term (β„Š x) a = refl
  comm-hom-term (node f t) a = goal
    where
    goal : h ⟨$⟩ (⟦ node f t βŸ§β‚ ⟨$⟩ a) β‰ˆ ⟦ node f t βŸ§β‚‚ ⟨$⟩ Ξ» i β†’ h ⟨$⟩ a i
    goal = begin
      h ⟨$⟩ (⟦ node f t βŸ§β‚ ⟨$⟩ a)                  β‰ˆβŸ¨ compatible (projβ‚‚ hh) ⟩
      (f ^ 𝑩)(Ξ» i β†’ h ⟨$⟩ (⟦ t i βŸ§β‚ ⟨$⟩ a))        β‰ˆβŸ¨ cong Interpβ‚‚ (≑.refl , Ξ» i β†’ comm-hom-term (t i) a) ⟩
      (f ^ 𝑩)(Ξ» i β†’ ⟦ t i βŸ§β‚‚ ⟨$⟩ Ξ» j β†’ h ⟨$⟩ a j)  β‰ˆβŸ¨ refl ⟩
      ⟦ node f t βŸ§β‚‚ ⟨$⟩ (Ξ» j β†’ h ⟨$⟩ a j)          ∎
```

#### 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.

```agda
_[_]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`.

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