---
layout: default
file: "src/Setoid/Varieties/Interpretation.lagda.md"
title: "Setoid.Varieties.Interpretation module"
date: "2026-06-15"
author: "the agda-algebras development team"
---

### Theory interpretations and the interpretability quasi-order

This is the [Setoid.Varieties.Interpretation][] module of the [Agda Universal Algebra Library][].

This module is to a theory interpretation what [Setoid.Varieties.Invariance][] is to
a signature morphism.  Where the latter packages a `SigMorphism` as a `reduct` with
respect to which satisfaction is an invariant, here we package an *interpretation*
([Overture.Terms.Interpretation][]) as a `reductα΄΅`{.AgdaFunction} and prove the
generalized satisfaction condition; we then use it to define the
**interpretability quasi-order** on equational theories and to record its reflexivity
and transitivity.

#### The interpretation reduct

For an interpretation `I : 𝑆₁ β†’ 𝑆₂` and an `𝑆₂`-algebra `𝑩`, the
*interpretation reduct* `reductα΄΅ I 𝑩` is the `𝑆₁`-algebra on the same carrier in
which each operation symbol `o` of `𝑆₁` is interpreted by the **derived operation**
`I o` β€” that is, by evaluating the `𝑆₂`-term `I o` in `𝑩`, reading the arguments as
the values of the argument positions of `o`.

When `I = ⟨ Ο† ⟩ᴡ` comes from a signature morphism, `reductα΄΅ I 𝑩` is the ordinary
`reduct Ο† 𝑩` (`reductα΄΅-⟨⟩`{.AgdaFunction} below, by `refl`), so this is the
term-valued generalization of [`reduct`][Setoid.Algebras.Reduct].

#### The satisfaction condition

The pay-off is the generalized satisfaction condition: for `𝑆₁`-terms `s , t`,

    reductα΄΅ I 𝑩 ⊧ s β‰ˆ t   if and only if   𝑩 ⊧ (I ✦ s) β‰ˆ (I ✦ t).

To check an `𝑆₁`-equation against the derived view of `𝑩` is to check the
*interpreted* equation against `𝑩` itself.  It is the shadow of one commuting
triangle of interpretation maps β€” naturality of the fold along the interpretation β€”
exactly as in [Setoid.Varieties.Invariance][], only now the node step
*grafts a derived term* rather than relabelling a symbol, and the proof leans on the
heterogeneous evaluation lemma `graft-eval`{.AgdaFunction} (evaluation commutes with
`graft`) in place of the definitional `reduct` step.  (As there, no clause matches a
concrete `Fin n`, so the without-K unifier is never asked to invert anything.)

#### The quasi-order

An equational theory `ℰ₁` of `𝑆₁` is *interpretable in* a theory `β„°β‚‚` of `𝑆₂`,
written `ℰ₁ β‰Ό β„°β‚‚`, when some interpretation carries every model of `β„°β‚‚` (via its
reduct) to a model of `ℰ₁`.  By the satisfaction condition this is the same as asking
that every `ℰ₁`-equation, *interpreted*, be a consequence of `β„°β‚‚`.

This is the universal algebraist's notion of one variety interpreting another, whose
order-reflection is the Garcia–Taylor lattice of interpretability types.[^1]

Reflexivity is the identity interpretation and transitivity is composition `_∘ᴡ_`;
the proofs are short *because* `✦-id` and `✦-∘` ([Setoid.Terms.Interpretation][])
already did the work, fed through the satisfaction condition.

This connects forward to planned formalizing work related to the Bodirsky–Pinsker
program, where interpretability between (infinite-domain) clones is the governing
relation.[^2]

A worked Maltsev-term instance is in [Classical.Interpretations.Maltsev][].

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

module Setoid.Varieties.Interpretation where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Agda.Primitive                 using () renaming ( Set to Type )
open import Data.Product                   using ( _,_ ; _Γ—_ ; Ξ£-syntax ; proj₁ ; projβ‚‚ )
open import Function                       using ( Func )
open import Level                          using ( Level )
open import Relation.Binary                using ( Setoid )

open import Relation.Binary.PropositionalEquality using ( _≑_ ; refl )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture.Signatures            using  ( π“ž ; π“₯ ; Signature
                                                  ; OperationSymbolsOf )
open import Overture.Signatures.Morphisms  using  ( SigMorphism )
open import Overture.Terms                 using  ( Term ; β„Š ; node )
open import Overture.Terms.Interpretation  using  ( Interpretation ; graft ; _✦_
                                                  ; idᴡ ; _∘ᴡ_ ; ⟨_⟩ᴡ )
open import Setoid.Algebras.Basic          using  ( Algebra ; _^_ ; 𝔻[_] ; π•Œ[_] )
open import Setoid.Algebras.Reduct         using  ( reduct )
open import Setoid.Terms.Basic             using  ( _≐_ ; ≐-isSym ; module Environment )
open import Setoid.Terms.Interpretation    using  ( ✦-id ; ✦-∘ )

import Setoid.Varieties.EquationalLogic as EqLogic

open Func using ( cong ) renaming ( to to _⟨$⟩_ )

private variable
  Ξ± ρ Ο‡ ΞΉ : Level
  X : Type Ο‡
  𝑆 𝑆₁ 𝑆₂ 𝑆₃ : Signature π“ž π“₯
  χ₁ Ο‡β‚‚ χ₃ ι₁ ΞΉβ‚‚ ι₃ : Level
```
-->

#### Two single-algebra lemmas

Everything in this block fixes one algebra `𝑨`.  First, satisfaction respects the
term equality `_≐_` on both sides.  (This is the convenience lemma we anticipated
consumers would want; the interpretability proofs are that consumer.)

```agda
module _ {𝑆 : Signature π“ž π“₯} (𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ) where
  open Environment 𝑨 using ( ⟦_⟧ ; ≐→Equal )
  open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ ) renaming ( refl to β‰ˆrefl ; sym to β‰ˆsym ; trans to β‰ˆtrans )
  open EqLogic {𝑆 = 𝑆} using ( _⊧_β‰ˆ_ )

  ⊧-≐ : {s sβ€² t tβ€² : Term {𝑆 = 𝑆} X}
    β†’ s ≐ sβ€² β†’ t ≐ tβ€² β†’ 𝑨 ⊧ s β‰ˆ t β†’ 𝑨 ⊧ sβ€² β‰ˆ tβ€²
  ⊧-≐ {s = s} {sβ€²} {t} {tβ€²} s≐sβ€² t≐tβ€² A⊧ Ξ· =
    β‰ˆtrans (β‰ˆsym (≐→Equal s sβ€² s≐sβ€² Ξ·)) (β‰ˆtrans (A⊧ Ξ·) (≐→Equal t tβ€² t≐tβ€² Ξ·))
```

Second, term evaluation commutes with `graft`: evaluating a grafted term is
evaluating the host term in the environment that first evaluates each grafted
subtree.  This is the heterogeneous-level analogue of the `substitution` lemma of
[Setoid.Terms.Basic][], and it is the node step of the interpretation triangle below.

```agda
  graft-eval : {ΞΎ : Level} {U : Type ΞΎ}
    (u : Term {𝑆 = 𝑆} U) (Οƒ : U β†’ Term {𝑆 = 𝑆} X) (Ξ· : X β†’ π•Œ[ 𝑨 ])
    β†’ ⟦ graft u Οƒ ⟧ ⟨$⟩ Ξ· β‰ˆ ⟦ u ⟧ ⟨$⟩ (Ξ» y β†’ ⟦ Οƒ y ⟧ ⟨$⟩ Ξ·)
  graft-eval (β„Š y)       Οƒ Ξ· = β‰ˆrefl
  graft-eval (node f us) Οƒ Ξ· = cong (Algebra.Interp 𝑨) (refl , Ξ» i β†’ graft-eval (us i) Οƒ Ξ·)
```

#### The interpretation reduct and the satisfaction condition

Now fix an interpretation `I` and an `𝑆₂`-algebra `𝑩`.  The reduct keeps the carrier
and interprets each `𝑆₁`-symbol `o` by evaluating `I o` (a derived operation), so its
`cong` is the congruence of that evaluation.

```agda
module _
  {𝑆₁ 𝑆₂ : Signature π“ž π“₯}
  (𝑩 : Algebra {𝑆 = 𝑆₂} Ξ± ρ)
  where
  module _
    (I : Interpretation 𝑆₁ 𝑆₂)
    where
    private module EnvB = Environment 𝑩
    open EnvB using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚‚ )
    open Algebra using (Domain ; Interp)

    reductα΄΅ : Algebra {𝑆 = 𝑆₁} Ξ± ρ
    reductα΄΅ .Domain = 𝔻[ 𝑩 ]
    reductα΄΅ .Interp ⟨$⟩ (o , args) = ⟦ I o βŸ§β‚‚ ⟨$⟩ args
    reductα΄΅ .Interp .cong {o , u} {.o , v} (refl , uβ‰ˆv) = cong ⟦ I o βŸ§β‚‚ uβ‰ˆv

    open Environment {𝑆 = 𝑆₁} reductα΄΅ using () renaming ( ⟦_⟧ to ⟦_βŸ§β‚ )
    open Setoid 𝔻[ 𝑩 ] using ( _β‰ˆ_ ) renaming ( refl to β‰ˆrefl ; sym to β‰ˆsym ; trans to β‰ˆtrans )
    open EqLogic {𝑆 = 𝑆₁} using () renaming ( _⊧_β‰ˆ_ to _βŠ§β‚_β‰ˆ_ )
    open EqLogic {𝑆 = 𝑆₂} using () renaming ( _⊧_β‰ˆ_ to _βŠ§β‚‚_β‰ˆ_ )
```

The interpretation triangle: evaluating an `𝑆₁`-term in the reduct equals evaluating its
interpretation in `𝑩`.  At a leaf both sides look up the variable.  At a node, the
reduct's interpretation *is* "evaluate the derived term `I f`", and the translation's
node clause grafts the interpreted subterms into `I f`; `graft-eval` says those agree,
and the inductive hypotheses match the arguments through `cong`.

```agda
    reductα΄΅-interp : (t : Term {𝑆 = 𝑆₁} X) (Ξ· : X β†’ π•Œ[ 𝑩 ]) β†’ ⟦ t βŸ§β‚ ⟨$⟩ Ξ· β‰ˆ ⟦ I ✦ t βŸ§β‚‚ ⟨$⟩ Ξ·
    reductα΄΅-interp (β„Š x) Ξ· = β‰ˆrefl
    reductα΄΅-interp (node f ts) Ξ· =
      β‰ˆtrans  (cong ⟦ I f βŸ§β‚‚ (Ξ» i β†’ reductα΄΅-interp (ts i) Ξ·))
              (β‰ˆsym (graft-eval 𝑩 (I f) (Ξ» i β†’ I ✦ ts i) Ξ·))
```

Satisfaction is the triangle quantified over environments, so each direction is a
`trans`-sandwich around the given satisfaction proof β€” verbatim the shape of
`⊧-reduct` / `⊧-expand`.  The equation sides are pinned (`{s}`/`{t}`), as the handoff
records, since `s` is not recoverable from `I ✦ s`.

```agda
    ⊧-interp : {s t : Term {𝑆 = 𝑆₁} X} β†’ 𝑩 βŠ§β‚‚ (I ✦ s) β‰ˆ (I ✦ t) β†’ reductα΄΅ βŠ§β‚ s β‰ˆ t
    ⊧-interp {s = s} {t} B⊧ η =
      β‰ˆtrans (reductα΄΅-interp s Ξ·) (β‰ˆtrans (B⊧ Ξ·) (β‰ˆsym (reductα΄΅-interp t Ξ·)))

    ⊧-uninterp : {s t : Term {𝑆 = 𝑆₁} X} β†’ reductα΄΅ βŠ§β‚ s β‰ˆ t β†’ 𝑩 βŠ§β‚‚ (I ✦ s) β‰ˆ (I ✦ t)
    ⊧-uninterp {s = s} {t} R⊧ η =
      β‰ˆtrans (β‰ˆsym (reductα΄΅-interp s Ξ·)) (β‰ˆtrans (R⊧ Ξ·) (reductα΄΅-interp t Ξ·))
```

#### `reductα΄΅` generalizes `reduct`

When the interpretation is the one induced by a signature morphism, its reduct *is*
the ordinary signature reduct, operation by operation, by `refl` β€” the algebra-level
witness that `_✦_` (and hence this whole development) extends to derived operations.

```agda
  reductα΄΅-⟨⟩ : {Ο† : SigMorphism 𝑆₁ 𝑆₂} {o : OperationSymbolsOf 𝑆₁}
    β†’ o ^ reductα΄΅ ⟨ Ο† ⟩ᴡ ≑ o ^ reduct Ο† 𝑩
  reductᴡ-⟨⟩ = refl
```

#### The interpretability quasi-order

A *theory* is an indexed family of equations.  `𝑨 βŠ¨β‚‘ β„°` is the assertion that `𝑨`
models every equation in `β„°`.

```agda
module _ {𝑆 : Signature π“ž π“₯} where
  open EqLogic {𝑆 = 𝑆} using ( _⊧_β‰ˆ_ )

  infix 4 _βŠ¨β‚‘_
  _βŠ¨β‚‘_ : {Idx : Type ΞΉ} β†’ Algebra Ξ± ρ β†’ (Idx β†’ Term X Γ— Term X) β†’ Type _
  𝑨 βŠ¨β‚‘ β„° = βˆ€ k β†’ 𝑨 ⊧ proj₁ (β„° k) β‰ˆ projβ‚‚ (β„° k)
```

Composition of interpretations carries through satisfaction.  This is the
reduct-level shadow of `✦-∘`: a `(J ∘ᴡ I)`-reduct satisfies exactly what the iterated
reduct `reductα΄΅ I (reductα΄΅ J π‘ͺ)` satisfies, by two applications of the satisfaction
condition and one `✦-∘` rewrite.  It is the engine of transitivity below.

```agda
module _
  {𝑆₁ 𝑆₂ 𝑆₃ : Signature π“ž π“₯}
  (I : Interpretation 𝑆₁ 𝑆₂)
  (J : Interpretation 𝑆₂ 𝑆₃)
  (π‘ͺ : Algebra {𝑆 = 𝑆₃} Ξ± ρ)
  where
  open EqLogic {𝑆 = 𝑆₁} using ( _⊧_β‰ˆ_ )

  reductα΄΅-∘-⊧ : {s t : Term {𝑆 = 𝑆₁} X}
    β†’ reductα΄΅ (reductα΄΅ π‘ͺ J) I ⊧ s β‰ˆ t β†’ reductα΄΅ π‘ͺ (J ∘ᴡ I) ⊧ s β‰ˆ t
  reductᴡ-∘-⊧ {s = s} {t} hyp =
    ⊧-interp π‘ͺ (J ∘ᴡ I) {s = s} {t}
      (⊧-≐ π‘ͺ (≐-isSym (✦-∘ s)) (≐-isSym (✦-∘ t))
        (⊧-uninterp π‘ͺ J {s = I ✦ s} {t = I ✦ t}
          (⊧-uninterp (reductα΄΅ π‘ͺ J) I {s = s} {t = t} hyp)))
```

`ℰ₁ β‰Ό β„°β‚‚` says `ℰ₁` (a theory of `𝑆₁`) is interpretable in `β„°β‚‚` (a theory of `𝑆₂`):
some interpretation's reduct sends every `β„°β‚‚`-model to an `ℰ₁`-model.  The relation is
indexed by the algebra-level pair `(α , ρ)` at which models are tested, exactly as the
satisfaction relations are.

```agda
module Interpret (α ρ : Level) where

  _β‰Ό_ : {𝑆₁ 𝑆₂ : Signature π“ž π“₯}
    {X₁ : Type χ₁} {Xβ‚‚ : Type Ο‡β‚‚} {Idx₁ : Type ι₁} {Idxβ‚‚ : Type ΞΉβ‚‚}
    β†’ (Idx₁ β†’ Term {𝑆 = 𝑆₁} X₁ Γ— Term {𝑆 = 𝑆₁} X₁)
    β†’ (Idxβ‚‚ β†’ Term {𝑆 = 𝑆₂} Xβ‚‚ Γ— Term {𝑆 = 𝑆₂} Xβ‚‚) β†’ Type _
  _β‰Ό_ {𝑆₁ = 𝑆₁} {𝑆₂ = 𝑆₂} ℰ₁ β„°β‚‚ =
    Ξ£[ I ∈ Interpretation 𝑆₁ 𝑆₂ ]
      ((𝑩 : Algebra {𝑆 = 𝑆₂} Ξ± ρ) β†’ 𝑩 βŠ¨β‚‘ β„°β‚‚ β†’ reductα΄΅ 𝑩 I βŠ¨β‚‘ ℰ₁)

  infix 4 _β‰Ό_
```

Reflexivity: the identity interpretation works, because `idᴡ ✦_` is the identity up
to `_≐_` (`✦-id`) and satisfaction respects `_≐_`.

```agda
module _ α ρ where

  open Interpret α ρ

  β‰Ό-refl : {𝑆 : Signature π“ž π“₯} {X : Type Ο‡} {Idx : Type ΞΉ}
    (β„° : Idx β†’ Term X Γ— Term X) β†’ β„° β‰Ό β„°
  β‰Ό-refl {𝑆 = 𝑆} β„° = idα΄΅ , red
    where
    red : (𝑩 : Algebra {𝑆 = 𝑆} Ξ± ρ) β†’ 𝑩 βŠ¨β‚‘ β„° β†’ reductα΄΅ 𝑩 idα΄΅ βŠ¨β‚‘ β„°
    red 𝑩 B⊨ k =
      ⊧-interp 𝑩 idα΄΅ {s = proj₁ (β„° k)} {t = projβ‚‚ (β„° k)}
        (⊧-≐ 𝑩 (≐-isSym (✦-id (β„° k .proj₁))) (≐-isSym (✦-id (β„° k .projβ‚‚))) (B⊨ k))
```

Transitivity: compose the interpretations with `_∘ᴡ_`, chain the two reduct
implications, and re-fold the iterated reduct into the composite reduct with
`reductᴡ-∘-⊧`.

```agda
  β‰Ό-trans : {𝑆₁ 𝑆₂ 𝑆₃ : Signature π“ž π“₯}
    {X₁ : Type χ₁} {Xβ‚‚ : Type Ο‡β‚‚} {X₃ : Type χ₃}
    {Idx₁ : Type ι₁} {Idxβ‚‚ : Type ΞΉβ‚‚} {Idx₃ : Type ι₃}
    (ℰ₁ : Idx₁ β†’ Term {𝑆 = 𝑆₁} X₁ Γ— Term {𝑆 = 𝑆₁} X₁)
    (β„°β‚‚ : Idxβ‚‚ β†’ Term {𝑆 = 𝑆₂} Xβ‚‚ Γ— Term {𝑆 = 𝑆₂} Xβ‚‚)
    (ℰ₃ : Idx₃ β†’ Term {𝑆 = 𝑆₃} X₃ Γ— Term {𝑆 = 𝑆₃} X₃)
    β†’ ℰ₁ β‰Ό β„°β‚‚ β†’ β„°β‚‚ β‰Ό ℰ₃ β†’ ℰ₁ β‰Ό ℰ₃

  β‰Ό-trans {𝑆₃ = 𝑆₃} ℰ₁ β„°β‚‚ ℰ₃ (I , Ihyp) (J , Jhyp) = J ∘ᴡ I , red
    where
    red : (π‘ͺ : Algebra {𝑆 = 𝑆₃} Ξ± ρ) β†’ π‘ͺ βŠ¨β‚‘ ℰ₃ β†’ reductα΄΅ π‘ͺ (J ∘ᴡ I) βŠ¨β‚‘ ℰ₁
    red π‘ͺ C⊨ k =
      reductα΄΅-∘-⊧ I J π‘ͺ {s = proj₁ (ℰ₁ k)} {t = projβ‚‚ (ℰ₁ k)}
        (Ihyp (reductα΄΅ π‘ͺ J) (Jhyp π‘ͺ C⊨) k)
```

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

[^1]: O. C. GarcΓ­a and W. Taylor, *The Lattice of Interpretability Types of Varieties*, Mem. Amer. Math. Soc. **50** (1984), no. 305.

[^2]: Infinitary CSP over Ο‰-categorical templates.