Presheaf Topos

PSh(Cat_tau): the presheaf topos. A presheaf assigns to each object a set (modeled as a predicate). Includes terminal/initial presheaves and pointwise product/coproduct operations.

Presheaf Topos

Summary

PSh(Cat_tau): the presheaf topos. A presheaf assigns to each object a set (modeled as a predicate). Includes terminal/initial presheaves and pointwise product/coproduct operations.

Statement

%
\label{def:presheaf-topos}
The \textbf{presheaf topos} of $\mathrm{Cat}_\tau$ is:
\[
    \boxed{%
    \mathrm{PSh}(\mathrm{Cat}_\tau)
    \;:=\;
    \bigl[\,
    \mathrm{Cat}_\tau^{\mathrm{op}},\;
    \mathbf{Set}
    \,\bigr],}
\]
the category of contravariant functors
$F : \mathrm{Cat}_\tau^{\mathrm{op}} \to \mathbf{Set}$
with natural transformations as morphisms.

A presheaf $F$ assigns:
\begin{itemize}
    \item to each object $X$,
          a set $F(X)$ (the ``sections over $X$'');
    \item to each arrow $f : X \to Y$
          (a divisibility witness $Y \mid X$),
          a restriction map
          $F(f) : F(Y) \to F(X)$.
\end{itemize}
These must satisfy functoriality:
$F(\id_X) = \id_{F(X)}$
and
$F(g \circ f) = F(f) \circ F(g)$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 132
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part14/ch55-limits-sites.tex lines 348-378

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Topos.LimitsSites
• Name: Tau.Topos.PShCatTau

Dependencies

• Canonical: I.D54, I.D55, I.D56

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.