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 (see Cubical.lagda).
{-# OPTIONS --without-K --exact-split --safe #-} module Setoid where open import Setoid.Overture open import Setoid.Relations open import Setoid.Algebras open import Setoid.Homomorphisms open import Setoid.Terms open import Setoid.Subalgebras open import Setoid.Varieties