Setoid.Functions

Setoid Functions

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

This is a barrel module: it declares nothing of its own and re-exports the five modules that develop functions between setoids. A setoid function is a map bundled with a proof that it respects the two equalities. That proof is about a single map, so it is only half of how the library does without function extensionality; the other half is that wherever two functions must be compared, an explicitly pointwise relation is used rather than propositional equality of functions. See function-equality of Setoid.Relations.Discrete and, for homomorphisms, _≋_ of Setoid.Categories.Algebra.

Guide to the submodules of Setoid.Functions

• Setoid.Functions.Basic: the identity, composition, and universe lifting of a setoid;
• Setoid.Functions.Injective: IsInjective and its composition law;
• Setoid.Functions.Surjective: IsSurjective, its composition law ⊙-IsSurjective, the right inverse SurjInv of a surjection, and epic-factor. The decidable-index projections proj and projIsOnto that ProjAlgIsOnto of Setoid.Algebras.Products consumes are not here; they are bare-types results in Overture.Functions;
• Setoid.Functions.Inverses: images and ranges, Image_∋_ and IsInRange;
• Setoid.Functions.Bijective: IsBijective as injective-and-surjective, with the inverse BijInv.

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

module Setoid.Functions where

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