Setoid.Categories.NaturalTransformation

Natural transformations between minimal functors

This is the Setoid.Categories.NaturalTransformation module of the Agda Universal Algebra Library.

A natural transformation is the third rung of the basic category-theory ladder, after Category and Functor, and it is the notion category theory was invented to make precise. Where a functor F : 𝐂 ⟶ 𝐃 translates one mathematical world into another, a natural transformation compares two such translations F, G : 𝐂 ⟶ 𝐃: it assigns to every object A of 𝐂 a 𝐃-morphism component A : F₀ A ⟶ G₀ A, in a way that is uniform in A.

Uniformity is the entire content of the definition. The components must not be ad-hoc choices made object by object; they must commute with every morphism of 𝐂, which the natural field states as the famous naturality square: for each f : A ⟶ B in 𝐂,

                component A
        F₀ A ───────────────→ G₀ A
          │                     │
     F₁ f │                     │ G₁ f
          ↓                     ↓
        F₀ B ───────────────→ G₀ B
                component B

both ways around the square are the same 𝐃-morphism — component B ∘ F₁ f equals G₁ f ∘ component A — up to the target category's hom-equality _≈_. Intuitively: first translate by F and then convert to G, or convert first and then translate by G; naturality says it cannot matter. A family of maps with this property is exactly what a working mathematician means by a construction that "requires no arbitrary choices."

The library has already met this notion twice, componentwise:

• A signature morphism φ : 𝑆₁ → 𝑆₂ induces the family ⟦ φ ⟧ A : ⟨ 𝑆₁ ⟩ A ⟶ ⟨ 𝑆₂ ⟩ A of Setoid.Signatures.Functor, whose naturality square (naturality) commutes by refl; reduct precomposes this family into an algebra's structure map.
• An adjunction carries two natural families, its unit and counit (Setoid.Categories.Adjunction), each with its naturality square recorded as a field.

This record packages the pattern once, so that constructions which consume a natural transformation whole — the Monad record of M4-5e is the inaugural consumer — can take one argument instead of a component family and a square. Where a componentwise rendering already is the canonical form (the Adjunction fields, the ⟦_⟧ family), it stays canonical; this record is the bundled view, not a replacement. (Adjunction derives unitNT / counitNT views for free.)

As with the rest of the layer (ADR-006), the record is minimal and self-contained — no agda-categories dependency — and every law is stated against the target category's hom-equality field _≈_, so categories with pointwise hom-setoids (the algebra categories Alg) prove naturality pointwise, with no function extensionality.

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

module Setoid.Categories.NaturalTransformation 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 )

private variable o ℓ e o′ ℓ′ e′ : Level

The record

A NaturalTransformation F G consists of the component family and its naturality square. The components live in the target category 𝐃, and so does the equality in which the square commutes.

record NaturalTransformation
  {𝐂 : Category o ℓ e} {𝐃 : Category o′ ℓ′ e′}
  (F G : Functor 𝐂 𝐃) : Type (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
  open Category 𝐂 renaming ( Obj to 𝐂₀ ; Hom to 𝐂[_,_] )
  open Category 𝐃 renaming ( Hom to 𝐃[_,_] ; _≈_ to _≈ᴰ_ ; _∘_ to _∘ᴰ_ )
  open Functor F renaming ( F₀ to F₀ ; F₁ to F₁ )
  open Functor G renaming ( F₀ to G₀ ; F₁ to G₁ )

  field
    -- One 𝐃-morphism per 𝐂-object: the A-th component F₀ A ⟶ G₀ A.
    component : (A : 𝐂₀) → 𝐃[ F₀ A , G₀ A ]

    -- The naturality square: the components commute with the image of
    -- every 𝐂-morphism, in the hom-equality of 𝐃.
    natural : {A B : 𝐂₀} (f : 𝐂[ A , B ]) → component B ∘ᴰ F₁ f ≈ᴰ G₁ f ∘ᴰ component A

A small dictionary for readers coming from the classical literature: what is written η : F ⟹ G with components η_A and square η_B ∘ F f = G f ∘ η_A appears here as η : NaturalTransformation F G with component η A and natural η f. Vertical and horizontal composition of natural transformations are not defined yet; per the library's two-consumer rule they will be added when a second construction needs them (the Monad laws below need only the components, which is also why the monad laws there are stated componentwise).