↑ Top

Equations and Varieties

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 #-}

module Base.Varieties where

open import Base.Varieties.EquationalLogic
open import Base.Varieties.Closure
open import Base.Varieties.Properties
open import Base.Varieties.Preservation
open import Base.Varieties.FreeAlgebras

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