Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Horizontal composites of natural transformations satisfy naturality

Statement

The horizontal composite of natural transformations satisfies the naturality equation.

Facts & Assumptions

Given: Natural transformations α:F⇒G:C→D\alpha:F\Rightarrow G:\mathcal C\to\mathcal D and β:H⇒L:D→E\beta:H\Rightarrow L:\mathcal D\to\mathcal E, and f:A→Bf:A\to B in C\mathcal C.

[L1]

Horizontal composition has component βGA∘H(αA)=L(αA)∘βFA\beta_{GA}\circ H(\alpha_A)=L(\alpha_A)\circ\beta_{FA}, and functors preserve composition (Whiskering and horizontal composition of natural transformations).

Proof

technique · direct
1.1

Naturality of β\beta at GfGf gives L(Gf)∘βGA=βGB∘H(Gf)L(Gf)\circ\beta_{GA}=\beta_{GB}\circ H(Gf), while functoriality sends the naturality equation Gf∘αA=αB∘FfGf\circ\alpha_A=\alpha_B\circ Ff to H(Gf)∘H(αA)=H(αB)∘H(Ff)H(Gf)\circ H(\alpha_A)=H(\alpha_B)\circ H(Ff).

givenL1
2.1

Combining these equations gives L(Gf)∘βGA∘H(αA)=βGB∘H(αB)∘H(Ff)L(Gf)\circ\beta_{GA}\circ H(\alpha_A)=\beta_{GB}\circ H(\alpha_B)\circ H(Ff).

step 1.1L1
3.1

The two outer composites are exactly L(Gf)∘(β∗α)AL(Gf)\circ(\beta*\alpha)_A and (β∗α)B∘H(Ff)(\beta*\alpha)_B\circ H(Ff), which proves naturality.

step 2.1L1∎

Depends on

Used by

Cited to discharge well-definedness by Whiskering and horizontal composition of natural transformations.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 5 results over 5 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources