---
layout: default
title : "Overture module"
date : "2022-17-06"
author: "the agda-algebras development team"
---

## Overture

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

The Overture is the foundation layer: the vocabulary every later tree (`Setoid/`,
`Classical/`) imports.  In re-export order:

+  [Overture.Preface][] is the front door: why the library exists, why Agda, and
   how to read what follows.
+  [Overture.Basic][] sets the logical foundations and shared preliminaries.

+  [Overture.Adjunction][] is the order-theoretic adjunction toolkit: closure,
   Galois connections, residuation.
+  [Overture.Cayley][] represents finite binary operations by Cayley tables, with
   decision procedures that discharge their laws.
+  [Overture.Counting][] proves the two counting-by-filtering lemmas, monotone and
   strict, that the library's well-founded descents on finite structures run on.
+  [Overture.Functions][] collects the raw-function infrastructure (images,
   computed inverses, surjectivity) that the `Setoid/` tree builds on.
+  [Overture.Operations][] represents an operation of arity `I` as a function
   from tuples `I → A` to `A`.
+  [Overture.Relations][] supplies the relation vocabulary, including the
   `Equivalence` bundle over a fixed carrier.
+  [Overture.Signatures][] defines the `Signature` type: operation symbols paired
   with an arity function.
+  [Overture.Terms][] gives terms over a signature, their interpretation, and
   translation along signature morphisms.

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

module Overture where

open import Overture.Preface     public
open import Overture.Basic       public

open import Overture.Adjunction  public
open import Overture.Cayley      public
open import Overture.Counting    public
open import Overture.Functions   public
open import Overture.Operations  public
open import Overture.Relations   public
open import Overture.Signatures  public
open import Overture.Terms       public
```