HolFun Associativity

HolFun composition is associative: (f1 o f2) o f3 = f1 o (f2 o f3). Follows from function extensionality. Together with identity and composition closure, HolFun forms a monoid.

HolFun Associativity

Summary

HolFun composition is associative: (f1 o f2) o f3 = f1 o (f2 o f3). Follows from function extensionality. Together with identity and composition closure, HolFun forms a monoid.

Statement

%
\label{prop:holfun-associativity}
Composition of HolFuns is associative:
for all $R, S, T \in \mathrm{HolFun}$,
\[
    \boxed{%
    (R \circ S) \circ T = R \circ (S \circ T).}
\]

Proof / Justification

This inherits directly from the associativity
of function composition,
which was already established
for the program monoid
(Theorem~\ref{thm:comp-assoc}, I.T03)
in Chapter~\ref{ch:program-monoid}.
The program monoid acts on $\tau$-Idx
by function application;
HolFun composition is a special case
of this action restricted to functions
that satisfy both D-holomorphy and tower coherence.
Since Theorem~\ref{thm:composition-closure} (I.T20)
guarantees that all intermediate compositions
remain in HolFun,
the associativity of the ambient function composition
restricts to HolFun without modification.

Source Context

• Registry source: book-01.jsonl line 118
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part13/ch51-diagonal-free-protection.tex lines 457-466

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Holomorphy.DiagonalProtection
• Name: Tau.Holomorphy.stagefun_comp_assoc

Dependencies

• Canonical: I.T20, I.T03

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.