Legacy.Base.Algebras

Algebra Types

This is the Legacy.Base.Algebras module of the Agda Universal Algebra Library in which we use type theory and Agda to codify the most basic objects of universal algebra, such as signatures, algebras, product algebras, congruence relations, and quotient algebras.

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

open import Overture  using ( 𝓞 ; 𝓥 ; Signature )

module Legacy.Base.Algebras {𝑆 : Signature 𝓞 𝓥 } where

open import Legacy.Base.Algebras.Basic        {𝑆 = 𝑆} public
open import Legacy.Base.Algebras.Products     {𝑆 = 𝑆} public
open import Legacy.Base.Algebras.Congruences  {𝑆 = 𝑆} public