↑ Top


Setoid Functions

This is the [Setoid.Functions][] module of the Agda Universal Algebra Library.

{-# OPTIONS --without-K --exact-split --safe #-}

module Setoid.Functions where

open import Setoid.Functions.Basic       public
open import Setoid.Functions.Inverses    public
open import Setoid.Functions.Injective   public
open import Setoid.Functions.Surjective  public
open import Setoid.Functions.Bijective   public


← Preface Setoid.Functions.Preliminaries →