Tau-Arrow

A tau-arrow from source to target is a HolFun (tau-holomorphic function). Two arrows are equal iff their underlying HolFuns agree extensionally at all inputs and stages.

Tau-Arrow

Summary

A tau-arrow from source to target is a HolFun (tau-holomorphic function). Two arrows are equal iff their underlying HolFuns agree extensionally at all inputs and stages.

Statement

%
\label{def:tau-arrow}
A \textbf{$\tau$-arrow} is an NF-equivalence class
of $\tau$-holomorphic programs:
\[
    \boxed{%
    \alpha = [\pi]_{\mathrm{NF}}
    \;:=\;
    \bigl\{\,
        \pi' \in \mathrm{HolProg}
        : \pi' \sim_{\mathrm{NF}} \pi
    \,\bigr\},}
\]
where $\mathrm{HolProg}$ denotes the set of programs
in the program monoid
(Definition~\ref{def:program-monoid}, I.D14)
whose induced $\omega$-germ transformer
is $\tau$-holomorphic
(Definition~\ref{def:holfun}, I.D47).

A $\tau$-arrow carries a unique HolFun:
if $\pi_1, \pi_2 \in [\pi]_{\mathrm{NF}}$,
then $\pi_1$ and $\pi_2$ induce the same
$\tau$-holomorphic function.
The arrow $\alpha$ is identified with this function:
\[
    T_\alpha := \text{the unique HolFun induced by any
    representative of } \alpha.
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 122
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part14/ch53-earned-arrows.tex lines 181-211

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Topos.EarnedArrows
• Name: Tau.Topos.TauArrow

Dependencies

• Canonical: I.D47, I.T21

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.