↑ 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 →