↑ Top

The Setoid Module of the Agda Universal Algebra Library

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

↑ Top Setoid.Overture →