---
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 --without-K --exact-split --safe #-}

module Setoid.Terms.Operations 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  ( OperationSymbolsOf ; ArityOf
                                             ; π“ž ; π“₯ ; Signature ; 𝑆 )
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 )
  open Setoid 𝔻[ 𝑨 ]   using ( _β‰ˆ_ ; refl )
  open Environment 𝑨   using ( ⟦_⟧ )

  free-lift-interp :  (Ξ· : X β†’ π•Œ[ 𝑨 ])(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 _ {𝑆 : Signature π“ž π“₯}{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

`interp-prod`{.AgdaFunction} says that interpreting a term in a product is the
same as interpreting it in each factor and collecting the results: for every term
`p` and every environment `ρ`, the value of `p` in `β¨… π’œ` under `ρ` agrees, at each
coordinate `i`, with the value of `p` in `π’œ i` under the `i`-th component of `ρ`.

This is the term-level counterpart of the way `β¨…`{.AgdaFunction} of
[Setoid.Algebras.Products][] interprets operation *symbols* in the first place,
and the proof is the induction that says so: the variable case is reflexivity, and
the operation case pushes the induction hypothesis through the product's
`Interp`{.AgdaField}.

```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 the most important fact about term operations
(`comm-hom-term`{.AgdaFunction}): every term commutes with every homomorphism.

```agda
module _
  {𝑆 : Signature π“ž π“₯}
  {𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρᡃ}
  {𝑩 : Algebra {𝑆 = 𝑆} Ξ² ρᡇ}
  ((h , hhom) : hom 𝑨 𝑩)
  where

  open Algebra 𝑩       using (Interp)
  open Setoid 𝔻[ 𝑩 ]  using ( _β‰ˆ_ ; refl )
  open Environment 𝑨   using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚ )
  open Environment 𝑩   using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚‚ )
  open SetoidReasoning 𝔻[ 𝑩 ]
  open IsHom

  comm-hom-term : (t : Term {𝑆 = 𝑆} X) (a : X β†’ π•Œ[ 𝑨 ])
    β†’ 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 (hhom) ⟩
      (f ^ 𝑩)(Ξ» i β†’ h ⟨$⟩ (⟦ t i βŸ§β‚ ⟨$⟩ a))        β‰ˆβŸ¨ cong Interp (≑.refl , Ξ» i β†’ comm-hom-term (t i) a) ⟩
      ⟦ 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 : {𝑆 : Signature π“ž π“₯}(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
```