Internal Hom

The internal hom Q^P: pointwise Boolean implication. (Q^P)(X) = true iff P(X) implies Q(X). This gives exponentials in E_tau.

Internal Hom

Summary

The internal hom Q^P: pointwise Boolean implication. (Q^P)(X) = true iff P(X) implies Q(X). This gives exponentials in E_tau.

Statement

%
\label{def:internal-hom}
Let $P, Q : \mathrm{Cat}_\tau^{\mathrm{op}} \to \mathrm{Set}$
be presheaves in $\mathcal{E}_\tau$
(Definition~\ref{def:earned-topos}, I.D59).
The \textbf{internal hom} (exponential)
$Q^P$ is the presheaf defined by:
\[
    \boxed{%
    (Q^P)(X)
    \;:=\;
    \mathrm{Nat}\bigl(y(X) \times P,\; Q\bigr)}
\]
for each object $X$ in $\mathrm{Cat}_\tau$,
where $y(X) = \Hom(-, X)$ is the representable presheaf
(Definition~\ref{def:yoneda-embedding}, I.D54)
and $\times$ denotes the product of presheaves
(Definition~\ref{def:categorical-product}, I.D60).

For a morphism $f : X_1 \to X_2$ in $\mathrm{Cat}_\tau$,
the restriction map
$(Q^P)(f) : (Q^P)(X_2) \to (Q^P)(X_1)$
sends a natural transformation
$\alpha : y(X_2) \times P \Rightarrow Q$
to the composite
$\alpha \circ (y(f) \times \id_P) :
y(X_1) \times P \Rightarrow Q$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 145
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part15/ch59-internal-hom.tex lines 118-146

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Topos.InternalHom
• Name: Tau.Topos.internal_hom

Dependencies

• Canonical: I.D60, I.D54

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.