This module collects all submodule of that part of the library based on setoids, as opposed to “bare” types (see Base.lagda), or Cubical Agda (used in the forthcoming cubical-agda-algebras library).
{-# OPTIONS --without-K --exact-split --safe #-} module Setoid where open import Setoid.Relations public open import Setoid.Functions public open import Setoid.Algebras public open import Setoid.Homomorphisms public open import Setoid.Terms public open import Setoid.Subalgebras public open import Setoid.Varieties public