---
layout: default
title : "Legacy.Base.Adjunction module (The Agda Universal Algebra Library)"
date : "2021-08-30"
author: "agda-algebras development team"
---

## <a id="adjunction">Adjunction</a>

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


```agda

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

module Legacy.Base.Adjunction where

open import Legacy.Base.Adjunction.Closure      public
open import Legacy.Base.Adjunction.Galois       public
open import Legacy.Base.Adjunction.Residuation  public
```