This is the Base.Structures.Terms module of the Agda Universal Algebra Library.
When we interpret a term in a structure we call the resulting
function a term operation. Given a term p and a structure ๐จ,
we denote by ๐จ โฆ p โง the interpretation of p in ๐จ.
This is defined inductively as follows.
If p is a variable symbol x : X and
if a : X โ โฃ ๐จ โฃ is a tuple of elements of โฃ ๐จ โฃ, then
define ๐จ โฆ p โง a := a x.
If p = f t, where f : โฃ ๐ โฃ is an operation symbol,
if t : (arity ๐น) f โ ๐ป X is a tuple of terms, and
if a : X โ โฃ ๐จ โฃ is a tuple from ๐จ, then
define ๐จ โฆ p โง a := (f แต ๐จ) (ฮป i โ ๐จ โฆ t i โง a).
Thus interpretation of a term is defined by structural induction.
{-# OPTIONS --without-K --exact-split --safe #-} module Base.Structures.Terms where -- Imports from Agda and the Agda Standard Library --------------------- open import Agda.Primitive using () renaming ( Set to Type ) open import Level using ( Level ) open import Base.Structures.Basic using ( signature ; structure ; _แต_ ) open import Base.Terms.Basic private variable ๐โ ๐ฅโ ๐โ ๐ฅโ ฯ ฮฑ ฯ : Level ๐น : signature ๐โ ๐ฅโ ๐ : signature ๐โ ๐ฅโ X : Type ฯ open signature open structure _โฆ_โง : (๐จ : structure ๐น ๐ {ฮฑ} {ฯ}) โ Term X โ (X โ carrier ๐จ) โ carrier ๐จ ๐จ โฆ โ x โง = ฮป a โ a x ๐จ โฆ node f t โง = ฮป a โ (f แต ๐จ) (ฮป i โ (๐จ โฆ t i โง ) a)