⚠️ Archived site. This is the pre-3.0 Agda Universal Algebra Library, preserved for reference. Its current home is agda-algebras.universalalgebra.org (as of July 2026).

↑ Top


Subalgebras over setoids

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


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

open import Overture using (𝓞 ; 𝓥 ; Signature)

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

open import Setoid.Subalgebras.Subuniverses  {𝑆 = 𝑆} public
open import Setoid.Subalgebras.Subalgebras   {𝑆 = 𝑆} public
open import Setoid.Subalgebras.Properties    {𝑆 = 𝑆} public

← Setoid.Terms.Properties Setoid.Subalgebras.Subuniverses →