Skip to content

Examples.Setoid

Worked examples over the Setoid universal-algebra layer

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

Whereas Examples/Classical/ pairs one worked instance with each concrete structure (magma, semigroup, monoid, โ€ฆ), the modules collected here exercise the generic Setoid/ universal-algebra machinery directly: free algebras over a signature, relatively free algebras / presentations, quotients by a congruence, and Birkhoff's HSP theorem specialized to a concrete algebra. They are the cross-structure and "richer" examples requested in issue #266.

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

module Examples.Setoid where

-- Each worked example defines its own local syntactic-product helper `_ยท_`, so they
-- must be opened without `public`: re-exporting would fail due to name clash.
-- This barrel keeps the five modules in the build and the documentation tree.
open import Examples.Setoid.FreeMagma
open import Examples.Setoid.FreeSemigroup
open import Examples.Setoid.Presentation
open import Examples.Setoid.FiniteQuotient
open import Examples.Setoid.HSPCommutativeMonoid