---
layout: default
file: "src/Overture/Terms/Translation.lagda.md"
title: "Overture.Terms.Translation module"
date: "2026-06-12"
author: "the agda-algebras development team"
---

### Translating terms along a signature morphism

This is the [Overture.Terms.Translation][] module of the [Agda Universal Algebra Library][].

A signature morphism `Ο† : SigMorphism 𝑆₁ 𝑆₂` ([Overture.Signatures.Morphisms][])
relabels operation symbols (`ΞΉ Ο†`, covariantly) and reindexes argument positions
(`ΞΊ Ο†`, contravariantly).  This module extends that relabelling from single symbols
to whole *terms*: the translation `Ο† ✢ t` rewrites an `𝑆₁`-term `t` into an
`𝑆₂`-term over the same variables, leaf by leaf and node by node.

The definition is exactly the structural recursion one would guess, and it is worth
reading the `node` clause slowly because the contravariance of `ΞΊ` is where all the
content lives.  A node `node f ts` of an `𝑆₁`-term carries one subterm `ts i` for
each position `i : ArityOf 𝑆₁ f`.  Its translation is a node labelled `ΞΉ Ο† f`, which
must carry one subterm for each position `j : ArityOf 𝑆₂ (ΞΉ Ο† f)` β€” a position of
the *target* symbol.  The position map `ΞΊ Ο† f` converts such a `j` back into a
source position `ΞΊ Ο† f j`, and the translated subterm at `j` is the translation of
`ts (ΞΊ Ο† f j)`:

```text
   𝑆₁-term:  node f ts          with subterms    ts i , i : ArityOf 𝑆₁ f
                  β”‚
                  β”‚  Ο† ✢_
                  ↓
   𝑆₂-term:  node (ΞΉ Ο† f) tsβ€²   with subterms    tsβ€² j = Ο† ✢ ts (ΞΊ Ο† f j) , j : ArityOf 𝑆₂ (ΞΉ Ο† f)
```

In the typical case of a signature *inclusion* β€” `ΞΉ` injective, each `ΞΊ Ο† f` the
identity, as in `Sig-Magma β†ͺ Sig-Monoid` β€” the translation simply re-reads a magma
term such as `(x βˆ™ y) βˆ™ z` as the same expression in the monoid signature.  That
"same expression, richer signature" reading is what makes the translation the
syntactic half of the *reduct*: `reduct Ο†` moves algebras from `𝑆₂` to `𝑆₁`
([Setoid.Algebras.Reduct][]), `Ο† ✢_` moves terms from `𝑆₁` to `𝑆₂`, and the
two are adjoint in the logical sense that satisfaction is invariant β€”
`reduct Ο† 𝑨 ⊧ s β‰ˆ t` iff `𝑨 ⊧ Ο† ✢ s β‰ˆ Ο† ✢ t` ([Setoid.Varieties.Invariance][]).
In the vocabulary of M4-5b, `Ο† ✢_` is the unique extension of the natural
transformation `⟦ Ο† ⟧ : ⟨ 𝑆₁ ⟩ ⟹ ⟨ 𝑆₂ ⟩` from single applications to free
`P_{𝑆₁}`-algebras; in monad vocabulary it is a *morphism of term monads*, a fact
recorded (up to `_≐_`) in [Setoid.Terms.Translation][].

Like `Term` itself, the translation presupposes only the signatures β€” no setoid, no
equality on any carrier β€” so it lives in `Overture/`.  Its laws (functoriality in
`Ο†`, congruence, and the substitution square) require the equality-of-terms relation
`_≐_` and are therefore stated in [Setoid.Terms.Translation][], mirroring the
`Overture.Terms` / `Setoid.Terms.Basic` split.  M4-5f will generalize precisely this
definition: a *theory interpretation* sends operation symbols to derived operations
(terms) rather than to symbols, and its action on terms replaces the `node` clause's
relabelling by substitution into the chosen derived term.

<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Overture.Terms.Translation where

open import Agda.Primitive                 using () renaming ( Set to Type )
open import Level                          using ( Level )
open import Overture.Signatures            using ( π“ž ; π“₯ ; Signature )
open import Overture.Signatures.Morphisms  using ( SigMorphism ; ΞΉ ; ΞΊ )

import Overture.Terms.Basic as Terms

private variable
  Ο‡ : Level
  X : Type Ο‡
```
-->

#### The translation

The two signatures are instantiated by module application; `Term₁ X` and
`Termβ‚‚ X` are the term types over the same variable type `X`.[^1]

```agda
module _ {𝑆₁ 𝑆₂ : Signature π“ž π“₯} where
  open Terms {𝑆 = 𝑆₁} using () renaming (β„Š to β„Šβ‚; node to node₁; Term to Term₁)
  open Terms {𝑆 = 𝑆₂} using () renaming (β„Š to β„Šβ‚‚; node to nodeβ‚‚; Term to Termβ‚‚)
  infix 15 _✢_

  _✢_ : SigMorphism 𝑆₁ 𝑆₂ β†’ Term₁ X β†’ Termβ‚‚ X
  Ο† ✢ β„Šβ‚ x = β„Šβ‚‚ x
  Ο† ✢ node₁ f ts = nodeβ‚‚ (ΞΉ Ο† f) (Ξ» j β†’ Ο† ✢ ts (ΞΊ Ο† f j))
```

Variables are fixed points of the translation (`Ο† ✢ β„Š x` is `β„Š x`, definitionally),
which is what lets environments transfer across it unchanged: interpreting `Ο† ✢ t`
needs values for exactly the variables that interpreting `t` needs.  The
reduct-invariance theorem leans on this directly.

--------------------------------------

[^1]: **Unicode tip**.  Type `\st` and select `✢` to get the star.