Alphabeta Math
TheoremStatement: 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 and vertical composition of natural transformations satisfy the interchange law

Statement

Whenever the expressions are defined,

(β′∘β)∗(α′∘α)=(β′∗α′)∘(β∗α).(\beta'\circ\beta)*(\alpha'\circ\alpha)=(\beta'*\alpha')\circ(\beta*\alpha).

Thus horizontal and vertical composition of natural transformations satisfy the interchange law.

Facts & Assumptions

Given: Natural transformations α:F⇒G\alpha:F\Rightarrow G, α′:G⇒K:C→D\alpha':G\Rightarrow K:\mathcal C\to\mathcal D and β:H⇒L\beta:H\Rightarrow L, β′:L⇒M:D→E\beta':L\Rightarrow M:\mathcal D\to\mathcal E.

[L1]

Vertical composition is componentwise and its composites are natural (Identity natural transformation and vertical composition, Vertical composites of natural transformations satisfy naturality); horizontal composition has the standard component formula and its composites are natural (Whiskering and horizontal composition of natural transformations, Horizontal composites of natural transformations satisfy naturality).

Proof

technique · direct
1.1

At an object AA, expand the left side by [L1] as βKA′∘βKA∘H(αA′)∘H(αA)\beta'_{KA}\circ\beta_{KA}\circ H(\alpha'_A)\circ H(\alpha_A).

givenL1
2.1

Naturality of β\beta at αA′:GA→KA\alpha'_A:GA\to KA gives βKA∘H(αA′)=L(αA′)∘βGA\beta_{KA}\circ H(\alpha'_A)=L(\alpha'_A)\circ\beta_{GA}. Substitution turns step 1.1 into (βKA′∘L(αA′))∘(βGA∘H(αA))(\beta'_{KA}\circ L(\alpha'_A))\circ(\beta_{GA}\circ H(\alpha_A)).

step 1.1L1
3.1

The two parenthesised factors are the AA-components of β′∗α′\beta'*\alpha' and β∗α\beta*\alpha, so every component agrees with the right side and the transformations are equal.

step 2.1L1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 8 results over 6 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