Setoid.Operations

Operations on setoids

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

It collects the setoid-level companions to the operation utilities of Overture.Operations. At present this is the single submodule Setoid.Operations.Properties, which generalizes the finite, propositional law-checkers of Overture.Operations.Properties to an arbitrary decidable setoid equipped with an exhaustive-search witness for its carrier.

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

module Setoid.Operations where

open import Setoid.Operations.Properties  public