↑ Top


Overture

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

The source code for this module comprises the (literate) Agda program that was used to generate the html page displaying the sentence you are now reading. This source code inhabits the file Base/Overture.lagda, which resides in the git repository of the agda-algebras library.

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

module Base.Functions where

open import Base.Functions.Inverses       public
open import Base.Functions.Injective      public
open import Base.Functions.Surjective     public
open import Base.Functions.Transformers   public


← Base Base.Functions.Preliminaries →