Skip to content

Setoid.Categories.Adjunction

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 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.

       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

{-# 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

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 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 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. ↩