This is the Base.Varieties module of the Agda Universal Algebra Library, where we define types for theories and their models, and for equational logic, and we prove properties of these types.

{-# OPTIONS --without-K --exact-split --safe #-} open import Overture using ( Signature ; 𝓞 ; 𝓥 ) module Base.Varieties {𝑆 : Signature 𝓞 𝓥} where open import Base.Varieties.EquationalLogic {𝑆 = 𝑆} public open import Base.Varieties.Closure {𝑆 = 𝑆} public open import Base.Varieties.Properties {𝑆 = 𝑆} public open import Base.Varieties.Preservation {𝑆 = 𝑆} public open import Level using ( Level ) module _ {α : Level} where open import Base.Varieties.FreeAlgebras {α = α} {𝑆 = 𝑆} public

← Base.Subalgebras.Properties Base.Varieties.EquationalLogic →