---
layout: default
file: "src/Setoid/Categories/Adjunction.lagda.md"
title: "Setoid.Categories.Adjunction module"
date: "2026-06-10"
author: "the agda-algebras development team"
---

### Adjunctions between minimal categories

This is the [Setoid.Categories.Adjunction][] module of the [Agda Universal Algebra Library][].

An `Adjunction L R` exhibits the functor `L : 𝐂 β†’ 𝐃` as *left adjoint* to
`R : 𝐃 β†’ 𝐂`.  As adjunctions are a central organizing concept, it's worth pausing to
understand exactly how they are used and what they are for.  The recurring situation
in algebra is a pair of translations running in opposite directions β€” a "free"
construction `L` and a "forgetful" one `R` β€” such that `L` provides the "most
economical" solution in 𝐃 to a problem posed in 𝐂.

A classical adjunction that appears in this library in
[Classical.Categories.AdjoinUnit][] is the following:

+  the forgetful functor `R` reduces a monoid to a semigroup;
+  the expansion functor `L` freely adjoins a unit to a semigroup;
+  the adjunction is the precise statement that `L 𝑺` is the universal monoid
   generated by the semigroup `𝑺`.

The last item means that each semigroup homomorphism from `𝑺` into (the underlying
semigroup of) a monoid, any monoid, `𝑴` extends uniquely to a monoid homomorphism
`L 𝑺 β†’ 𝑴`.

Following the architecture design record [ADR-006][], the `Adjunction`{.AgdaRecord}
record presents this with unit and counit, *componentwise*, that is, a family `unit`
of 𝐂-morphisms `A β†’ R (L A)` and a family `counit` of 𝐃-morphisms `L (R B) β†’ B`,
each with its naturality square.

The two families have direct readings.

+  `unit A : A β†’ R (L A)` embeds `A` into (the underlying-𝐂-object of) its free
   object; "every generator is an element of the free thing it generates;" for
   `adjoinUnit ⊣ forgetUnit` the unit is the inclusion `just`.

+  `counit B : L (R B) β†’ B` *evaluates*: build the free object on something that
   already was a 𝐃-object and there is a canonical map collapsing the formal
   structure back onto the real one; for `adjoinUnit ⊣ forgetUnit` the counit sends
   the freshly adjoined unit to the `Ξ΅` of `B`.

The two *triangle identities* `zig` and `zag` say the unit and counit are inverse
*up to one application of `L` or `R`*.

```text

       L (unit A)                    unit (R B)
   L A ────────→ L (R (L A))     R B ────────→ R (L (R B))
       β•²         β”‚                   β•²         β”‚
        β•²        β”‚                    β•²        β”‚
      id β•²       β”‚ counit           id β•²       β”‚ R (counit B)
          β•²      β”‚  (L A)               β•²      β”‚
           β•²     β”‚                       β•²     β”‚
            β•²    β”‚                        β•²    β”‚
             β•²   β”‚                         β•²   β”‚
              β†˜  ↓                          β†˜  ↓
               L A                           R B
```

The following two coherences are what entitle one to call `L` *the* free
construction rather than merely *a* section of `R`:[^1]

+  `zig` (left): embed the generators of `L A` and then evaluate to get `L A` back.
+  `zag` (right): embed `R B` into the free object over it and then evaluate inside
   `R` to get `R B` back.

Every law is stated against the owning category's hom-equality `_β‰ˆ_`, so an
instance whose hom-equality is pointwise (the algebra categories of
[Setoid.Categories.Algebra][]) proves the triangles pointwise, with no funext.[^2]

<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Categories.Adjunction where

open import Agda.Primitive  using ( _βŠ”_ ) renaming ( Set to Type )
open import Level           using ( Level )

open import Setoid.Categories.Category               using ( Category )
open import Setoid.Categories.Functor                using ( Functor ; idF ; _∘F_ )
open import Setoid.Categories.NaturalTransformation  using ( NaturalTransformation )

private variable o β„“ e oβ€² β„“β€² eβ€² : Level
```
-->

```agda
record Adjunction
  {𝐂 : Category o β„“ e} {𝐃 : Category oβ€² β„“β€² eβ€²}
  (L : Functor 𝐂 𝐃) (R : Functor 𝐃 𝐂) : Type (o βŠ” β„“ βŠ” e βŠ” oβ€² βŠ” β„“β€² βŠ” eβ€²) where
  open Category 𝐂 renaming ( Obj to 𝐂₀; Hom to 𝐂[_,_]; _β‰ˆ_ to _β‰ˆα΅ˆα΅’α΅_; id to idα΅ˆα΅’α΅; _∘_ to _βˆ˜α΅ˆα΅’α΅_ )
  open Category 𝐃 renaming ( Obj to 𝐃₀; Hom to 𝐃[_,_]; _β‰ˆ_ to _β‰ˆαΆœα΅’α΅ˆ_; id to idαΆœα΅’α΅ˆ; _∘_ to _βˆ˜αΆœα΅’α΅ˆ_ )
  open Functor L using () renaming ( Fβ‚€ to Lβ‚€ ; F₁ to L₁ )
  open Functor R using () renaming ( Fβ‚€ to Rβ‚€ ; F₁ to R₁ )

  field
    -- The unit: for each object A of 𝐂, a morphism A β†’ R (L A).
    unit : (A : 𝐂₀) β†’ 𝐂[ A , Rβ‚€ (Lβ‚€ A) ]
    -- The counit: for each object B of 𝐃, a morphism L (R B) β†’ B.
    counit : (B : 𝐃₀) β†’ 𝐃[ Lβ‚€ (Rβ‚€ B) , B ]

  -- Ξ· and Ξ΅ are the traditional names for the unit and counit components; we expose
  -- them as derived shorthands (mirroring Monad's Ξ· / ΞΌ), so that proofs may use the
  -- standard notation while the self-documenting `unit` / `counit` stay canonical.
  -- Being derived rather than fields, a consumer who also has an environment `Ξ·` or a
  -- monoid identity `Ξ΅` in scope can simply decline to bring these into scope.
  Ξ· = unit
  Ξ΅ = counit

  field
    -- Naturality of each family.
    unit-natural : {A B : 𝐂₀} (f : 𝐂[ A , B ]) β†’ unit B βˆ˜α΅ˆα΅’α΅ f β‰ˆα΅ˆα΅’α΅ R₁ (L₁ f) βˆ˜α΅ˆα΅’α΅ unit A
    counit-natural : {A B : 𝐃₀} (g : 𝐃[ A , B ]) β†’ counit B βˆ˜αΆœα΅’α΅ˆ L₁ (R₁ g) β‰ˆαΆœα΅’α΅ˆ g βˆ˜αΆœα΅’α΅ˆ counit A

    -- The triangle identities.
    zig : (A : 𝐂₀) β†’ counit (Lβ‚€ A) βˆ˜αΆœα΅’α΅ˆ L₁ (unit A) β‰ˆαΆœα΅’α΅ˆ idαΆœα΅’α΅ˆ {Lβ‚€ A}
    zag : (B : 𝐃₀) β†’ R₁ (counit B) βˆ˜α΅ˆα΅’α΅ unit (Rβ‚€ B) β‰ˆα΅ˆα΅’α΅ idα΅ˆα΅’α΅ {Rβ‚€ B}

  -- The unit and counit, packaged as natural transformations (the bundled views);
  -- the componentwise fields above remain canonical.
  unitNT : NaturalTransformation (idF {𝐂 = 𝐂}) (R ∘F L)
  unitNT = record { component = unit ; natural = unit-natural }

  counitNT : NaturalTransformation (L ∘F R) (idF {𝐂 = 𝐃})
  counitNT = record { component = counit ; natural = counit-natural }
```

The derived members `unitNT` and `counitNT` repackage the componentwise data as
[`NaturalTransformation`][Setoid.Categories.NaturalTransformation] records; `unitNT` is
the unit natural transformation from the identity functor to the composite `R ∘F L`;
`counitNT` is the counit natural transformation from `L ∘F R` to the identity.

Note there is nothing to prove: the naturality squares demanded by the records are
*definitionally* the `unit-natural` and `counit-natural` fields.

The composite `R ∘F L`, equipped with `unitNT` as its unit, is in fact a monad on 𝐂,
with multiplication `R₁ (counit (Lβ‚€ A))`; that classical theorem is `adjunctionβ†’monad` in
[Setoid.Categories.Monad][].

--------------------------------------

[^1]: The design note [m4-5d-free-expansion.md](docs/notes/m4-5d-free-expansion.md) develops that contrast (a section chooses, an adjoint adjoins) at length.

[^2]: The natural-transformation record this footnote once deferred to M4-5e now exists ([Setoid.Categories.NaturalTransformation][]), and `unitNT` / `counitNT` below provide the bundled views.  The componentwise fields remain the canonical form, both because they are what the free-expansion spike of M4-5d consumes and because componentwise data is what concrete instances can supply pointwise without funext.

[ADR-006]: docs/adr/006-signature-morphism-category.md