---
layout: default
title : "Legacy.Base.Functions module (Agda Universal Algebra Library)"
date : "2021-01-12"
author: "the agda-algebras development team"
---

## <a id="functions">Functions</a>

This is the [Legacy.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 [Legacy/Base/Functions.lagda][], which resides in the
[git repository of the agda-algebras library][].


```agda


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

module Legacy.Base.Functions where

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