This is the 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 #-} module Varieties where open import Varieties.EquationalLogic open import Varieties.Closure open import Varieties.Properties open import Varieties.Preservation open import Varieties.FreeAlgebras open import Varieties.Func