Natural Transformation

A natural transformation between tau-functors. In a thin category, naturality is AUTOMATIC: the naturality square commutes because there is at most one arrow in each direction.

Natural Transformation

Summary

A natural transformation between tau-functors. In a thin category, naturality is AUTOMATIC: the naturality square commutes because there is at most one arrow in each direction.

Statement

%
\label{def:natural-transformation}
Let $F, G : \mathrm{Cat}_\tau \to \mathrm{Cat}_\tau$
be $\tau$-functors.
A \textbf{natural transformation}
$\eta : F \Rightarrow G$
is a family of $\tau$-arrows
\[
    \bigl\{\, \eta_X : F(X) \to G(X) \,\bigr\}_{X \in \mathrm{Obj}(\mathrm{Cat}_\tau)}
\]
such that for every morphism $f : X \to Y$,
the \textbf{naturality square} commutes:
\[
    \boxed{%
    \begin{array}{ccc}
        F(X) & \xrightarrow{\;\eta_X\;} & G(X) \\
        \downarrow\scriptstyle{F(f)} & & \downarrow\scriptstyle{G(f)} \\
        F(Y) & \xrightarrow{\;\eta_Y\;} & G(Y)
    \end{array}
    \qquad
    G(f) \circ \eta_X = \eta_Y \circ F(f).}
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 127
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part14/ch54-functors.tex lines 186-209

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Topos.Functors
• Name: Tau.Topos.NatTrans

Dependencies

• Canonical: I.D52

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.