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

↑ Top Setoid.Relations →