Tau-Functor

A tau-functor maps objects to objects. In thin Cat_tau, functors are determined by their object map alone (at most one morphism between any pair, so the morphism map is uniquely determined).

Tau-Functor

Summary

A tau-functor maps objects to objects. In thin Cat_tau, functors are determined by their object map alone (at most one morphism between any pair, so the morphism map is uniquely determined).

Statement

%
\label{def:tau-functor}
A \textbf{$\tau$-functor}
$F : \mathrm{Cat}_\tau \to \mathrm{Cat}_\tau$
consists of:
\begin{enumerate}
    \item An \textbf{object map}
          $F_0 : \tau\text{-Idx} \to \tau\text{-Idx}$.
    \item A \textbf{morphism map}:
          for every $\tau$-arrow $f : X \to Y$,
          a $\tau$-arrow $F(f) : F_0(X) \to F_0(Y)$.
\end{enumerate}
These maps must satisfy:
\begin{enumerate}
    \item[(F1)] \textbf{Identity preservation}:
          $F(\mathrm{id}_X) = \mathrm{id}_{F_0(X)}$
          for every object $X$.
    \item[(F2)] \textbf{Composition preservation}:
          $F(g \circ f) = F(g) \circ F(f)$
          for every composable pair
          $f : X \to Y$, $g : Y \to Z$.
\end{enumerate}
\[
    \boxed{%
    F : \mathrm{Cat}_\tau \to \mathrm{Cat}_\tau
    \quad\text{preserves}\quad
    \mathrm{id} \;\text{and}\; \circ.}
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: I.D51

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.