Setoid.Algebras

Setoid Representation of Algebras

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

This is a barrel module: it declares nothing of its own and re-exports the four modules that define algebras over setoids. An algebra here is a setoid together with an interpretation of every operation symbol as a setoid function on it, so that each operation respects the carrier's equivalence; ADR-001 records why that, rather than a bare type under propositional equality, is the canonical representation.

Submodule guide

• Setoid.Algebras.Basic: the Algebra record, the smart constructors mkAlgebra and mkAlgebraₚ, the interpretation operator _^_, the domain and carrier projections 𝔻[_] and 𝕌[_], and universe lifting;
• Setoid.Algebras.Products: products of indexed families and of classes;
• Setoid.Algebras.Finite: the FiniteAlgebra interface;
• Setoid.Algebras.Reduct: reducts along a signature morphism, and their functoriality.

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

module Setoid.Algebras where

open import Setoid.Algebras.Basic     public
open import Setoid.Algebras.Finite    public
open import Setoid.Algebras.Products  public
open import Setoid.Algebras.Reduct    public