Setoid.Terms

Terms on setoids

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

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

open import Overture using (𝓞 ; 𝓥 ; Signature)

module Setoid.Terms {𝑆 : Signature 𝓞 𝓥} where

open import Setoid.Terms.Basic       {𝑆 = 𝑆}  public
open import Setoid.Terms.Interpretation       public
open import Setoid.Terms.Monad       {𝑆 = 𝑆}  public
open import Setoid.Terms.Operations  {𝑆 = 𝑆}  public
open import Setoid.Terms.Properties  {𝑆 = 𝑆}  public
open import Setoid.Terms.Translation          public

(The two-signature modules Setoid.Terms.Translation and Setoid.Terms.Interpretation relate two signatures at once, so they are not {𝑆}-parameterized; they are nonetheless re-exported here for convenience.)