⚠️ Archived site. This is the pre-3.0 Agda Universal Algebra Library, preserved for reference. Its current home is agda-algebras.universalalgebra.org (as of July 2026).

↑ Top

Overture

This is the [Base.Overture][] 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.Overture where

open import Base.Overture.Preliminaries
open import Base.Overture.Inverses
open import Base.Overture.Injective
open import Base.Overture.Surjective
open import Base.Overture.Transformers

← Base Base.Overture.Preliminaries →