↑ Top

---

Equations and Varieties for Setoids

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

{-# OPTIONS --without-K --exact-split --safe #-}

open import Overture using (𝓞 ; 𝓥 ; Signature)

module Setoid.Varieties {𝑆 : Signature 𝓞 𝓥} where

open import Setoid.Varieties.EquationalLogic   {𝑆 = 𝑆} public
open import Setoid.Varieties.SoundAndComplete  {𝑆 = 𝑆} public
open import Setoid.Varieties.Closure           {𝑆 = 𝑆} public
open import Setoid.Varieties.Properties        {𝑆 = 𝑆} public
open import Setoid.Varieties.Preservation      {𝑆 = 𝑆} public
open import Setoid.Varieties.FreeAlgebras      {𝑆 = 𝑆} public
open import Setoid.Varieties.HSP               {𝑆 = 𝑆} public

---

← Setoid.Subalgebras.Properties Setoid.Varieties.EquationalLogic →