---
layout: default
title : "Setoid.Varieties module (Agda Universal Algebra Library)"
date : "2021-07-26"
author: "agda-algebras development team"
---

### Equations and Varieties for Setoids

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


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

open import Overture using (𝓞 ; 𝓥 ; Signature)

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

open import Setoid.Varieties.Closure           {𝑆 = 𝑆}  public
open import Setoid.Varieties.EquationalLogic   {𝑆 = 𝑆}  public
open import Setoid.Varieties.FreeAlgebras      {𝑆 = 𝑆}  public
open import Setoid.Varieties.FreeSubstitution  {𝑆 = 𝑆}  public
open import Setoid.Varieties.HSP               {𝑆 = 𝑆}  public
open import Setoid.Varieties.Interpretation             public
open import Setoid.Varieties.Invariance                 public
open import Setoid.Varieties.Invariants        {𝑆 = 𝑆}  public
open import Setoid.Varieties.Maltsev                    public
open import Setoid.Varieties.Preservation      {𝑆 = 𝑆}  public
open import Setoid.Varieties.Properties        {𝑆 = 𝑆}  public
open import Setoid.Varieties.Reducts                    public
open import Setoid.Varieties.SoundAndComplete  {𝑆 = 𝑆}  public
```