Skip to content

Setoid.Terms.Translation

Laws of term translation

This is the Setoid.Terms.Translation module of the Agda Universal Algebra Library.

The translation Ο† ✢ t of terms along a signature morphism is defined in Overture.Terms.Translation, where it needs nothing but the signatures. Its laws, proved here, compare functions on node positions (Ξ» i β†’ …) and therefore live at the level of the equality-of-terms relation _≐_ of Setoid.Terms.Basic β€” the same division of labor as Term (Overture) versus 𝑻 X and _≐_ (Setoid). None of the laws below can be strengthened to propositional _≑_ under --safe: each compares position functions that agree pointwise but are not definitionally equal, which is exactly the situation _≐_ exists for.

Together the laws say that _✢_ is as well-behaved as it could possibly be β€” it is a functorial family of monad morphisms:

  • ✢-cong β€” translation respects term equality, so Ο† ✢_ is a setoid function between term setoids (✢-func packages it as a Func).
  • ✢-id and ✢-∘ β€” translating along the identity morphism changes nothing, and translating along a composite is translating twice: the assignment Ο† ↦ Ο† ✢_ is a functor from the category Sig of signatures (Overture.Signatures.Morphisms) to term-setoid endomaps. This lifts the functoriality of ⟦_⟧ (single applications, Setoid.Signatures.Functor) from one operation deep to arbitrarily deep terms.
  • ✢-sub β€” the monad morphism square: translating after substituting is substituting after translating,
                    _[ Οƒ ]
     Term₁ Y ──────────────────────→ Term₁ X

        β”‚                             β”‚
   Ο† ✢_ β”‚                             β”‚ Ο† ✢_
        ↓                             ↓
     Termβ‚‚ Y ──────────────────────→ Termβ‚‚ X
              _[ (Ξ» y β†’ Ο† ✢ Οƒ y) ]

where the bottom edge substitutes the translated terms. In monad vocabulary (Setoid.Terms.Monad), Ο† ✢_ commutes with the units (definitionally β€” Ο† ✢ β„Š x is β„Š x) and with the multiplications (this square), which is the definition of a morphism between the term monads of 𝑆₁ and 𝑆₂. Equivalently, it is a functor between their Kleisli categories that is the identity on objects.

Looking one subissue ahead: M4-5f's theory interpretations replace the symbol-to-symbol ΞΉ by a symbol-to-derived-term assignment, and ✢-sub is the law that makes interpretations compose β€” substitute first or interpret first, same result.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Terms.Translation where

open import Agda.Primitive                 using () renaming ( Set to Type )

-- Imports from the Agda Standard Library ----------------------------
open import Function                       using ( Func )
open import Level                          using ( Level )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture.Signatures            using ( π“ž ; π“₯ ; Signature )
open import Overture.Signatures.Morphisms  using ( SigMorphism ; ΞΉ ; ΞΊ ; id-morphism ; _βˆ˜β‚›_ )
open import Overture.Terms                 using ( Term ; β„Š ; node )
open import Overture.Terms.Translation     using ( _✢_ )
open import Setoid.Terms.Basic             using ( _≐_ ; ≐-isRefl ; Sub ; _[_] ; TermSetoid )

open _≐_ using ( rfl ; gnl )
open Func using ( cong ) renaming ( to to _⟨$⟩_ )

private variable
  Ο‡ : Level
  X Y : Type Ο‡
Congruence: translation is a setoid function

Equal terms translate to equal terms. The leaf case is immediate (translation fixes variables); at a node, the inductive hypotheses are consulted at the reindexed positions, mirroring the node clause of _✢_ itself.

module _ {𝑆₁ 𝑆₂ : Signature π“ž π“₯} {Ο† : SigMorphism 𝑆₁ 𝑆₂} where

  ✢-cong : {s t : Term {𝑆 = 𝑆₁} X} β†’ s ≐ t β†’ (Ο† ✢ s) ≐ (Ο† ✢ t)
  ✢-cong (rfl x≑y) = rfl x≑y
  ✢-cong (gnl {f = f} ps) = gnl (Ξ» j β†’ ✢-cong (ps (ΞΊ Ο† f j)))

  -- The packaged form: translation as a map of term setoids.
  ✢-func : (X : Type Ο‡) β†’ Func (TermSetoid {𝑆 = 𝑆₁} X) (TermSetoid {𝑆 = 𝑆₂} X)
  ✢-func X ⟨$⟩ t = Ο† ✢ t
  ✢-func X .cong = ✢-cong
The monad-morphism square

Translation commutes with substitution. (It commutes with the units by definition: Ο† ✢ β„Š x reduces to β„Š x.)

  ✢-sub : (t : Term {𝑆 = 𝑆₁} Y) (Οƒ : Sub {𝑆 = 𝑆₁} X Y)
    β†’ Ο† ✢ t [ Οƒ ] ≐ (Ο† ✢ t) [ (Ξ» y β†’ Ο† ✢ Οƒ y) ]
  ✢-sub (β„Š y) Οƒ = ≐-isRefl
  ✢-sub (node f ts) Οƒ = gnl (Ξ» j β†’ ✢-sub (ts (ΞΊ Ο† f j)) Οƒ)
Functoriality in the signature morphism

Translating along the identity signature morphism is the identity (up to _≐_ β€” the node clause rebuilds the position function, so the two sides are pointwise, not definitionally, equal), and translating along a composite is the composite of the translations.

module _ {𝑆 : Signature π“ž π“₯} where

  ✢-id : (t : Term {𝑆 = 𝑆} X) β†’ (id-morphism ✢ t) ≐ t
  ✢-id (β„Š x) = ≐-isRefl
  ✢-id (node f ts) = gnl (Ξ» i β†’ ✢-id (ts i))


module _ {𝑆₁ 𝑆₂ 𝑆₃ : Signature π“ž π“₯} {Ο† : SigMorphism 𝑆₁ 𝑆₂} {ψ : SigMorphism 𝑆₂ 𝑆₃} where

  ✢-∘ : (t : Term {𝑆 = 𝑆₁} X) β†’ (ψ βˆ˜β‚› Ο†) ✢ t ≐ ψ ✢ (Ο† ✢ t)
  ✢-∘ (β„Š x) = ≐-isRefl
  ✢-∘ (node f ts) = gnl (Ξ» i β†’ ✢-∘ (ts (ΞΊ Ο† f (ΞΊ ψ (ΞΉ Ο† f) i))))