Earned Topos

The earned topos E_tau = PSh(Cat_tau) with Omega_tau as subobject classifier. Bundles the Grothendieck topos structure with the four-valued classifier and truth arrow.

Earned Topos

Summary

The earned topos E_tau = PSh(Cat_tau) with Omega_tau as subobject classifier. Bundles the Grothendieck topos structure with the four-valued classifier and truth arrow.

Statement

%
\label{def:earned-topos}
The \textbf{earned topos} is the Grothendieck topos
\[
    \boxed{%
    \mathcal{E}_\tau
    := \bigl(\mathrm{PSh}(\mathrm{Cat}_\tau),\;
    \Omega_\tau,\;
    \mathrm{true} : 1 \to \Omega_\tau\bigr),}
\]
where:
\begin{enumerate}
    \item $\mathrm{PSh}(\mathrm{Cat}_\tau)$
          is the presheaf topos
          (Definition~\ref{def:presheaf-topos}, I.D57).
    \item $\Omega_\tau = \mathrm{Truth4}$
          is the subobject classifier
          (Theorem~\ref{thm:omega-tau-classifier}, I.T25).
    \item $\mathrm{true} : 1 \to \Omega_\tau$,
          $* \mapsto \mathsf{T}$
          (Definition~\ref{def:omega-tau}, I.D41).
\end{enumerate}
The earned topos possesses
finite limits (Chapter~\ref{ch:limits-sites}),
a subobject classifier (this chapter),
and exponentials
(earned in Chapter~\ref{ch:internal-hom}, Part~XIV).

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 137
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part14/ch56-earned-topos.tex lines 338-366

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Topos.EarnedTopos
• Name: Tau.Topos.EarnedTopos

Dependencies

• Canonical: I.D57, I.T24, I.T25, I.D58

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.