Alphabeta Math
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.

✓ 6 results · all verified · 6 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 6 also cleared it.

Strictification and Mac Lanes Coherence Theorem - Examples

1 · Prerequisites

2 · Summary

These examples make the coherence theorem concrete. They write out canonical comparison maps, display the free word category at small length, and compute the strictification functor in a familiar cartesian case.

The counterexample on this page is the page's guardrail: formal vertices can collapse to one object in a specific monoidal category, and once that happens a noncanonical endomorphism can spoil commutativity.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The two routes around the pentagon are equal

Example

For objects A,B,C,D in a monoidal category, the pentagon compares two canonical composites from ((A⊗B)⊗C)⊗D to A⊗(B⊗(C⊗D)).

Facts & Assumptions

Given: Four objects A,B,C,D in a monoidal category.

[L1]

Between any two parenthesisations of the same ordered tensor word, there is a unique canonical natural isomorphism (Mac Lane coherence in canonical-map form).

Verification

technique · direct
1.1given

One route around the pentagon is the composite ((A⊗B)⊗C)⊗D→αA⊗B,C,D(A⊗B)⊗(C⊗D)→αA,B,C⊗DA⊗(B⊗(C⊗D)).

1.2given

The other route is the composite ((A⊗B)⊗C)⊗D→αA,B,C⊗1D(A⊗(B⊗C))⊗D→αA,B⊗C,DA⊗((B⊗C)⊗D)→1A⊗αB,C,DA⊗(B⊗(C⊗D)).

2.1L1step 1.1step 1.2∎

Both composites are canonical morphisms with the same source and target, so [L1] makes them equal.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

A canonical map between two bracketings of a five-fold product

Example

Take the two parenthesisations u:=((A⊗(B⊗C))⊗(D⊗E)),v:=A⊗(B⊗(C⊗(D⊗E))). A canonical map u→v is obtained by associators alone.

Facts & Assumptions

Given: Objects A,B,C,D,E of a monoidal category.

[L1]

Between any two parenthesisations of one ordered tensor word there is a unique canonical natural isomorphism (Mac Lane coherence in canonical-map form).

Verification

technique · direct
1.1given

Apply the outer associator to obtain ((A⊗(B⊗C))⊗(D⊗E))→αA,B⊗C,D⊗EA⊗((B⊗C)⊗(D⊗E)).

2.1step 1.1

Apply 1A⊗αB,C,D⊗E to the result of step 1.1 and get A⊗((B⊗C)⊗(D⊗E))→A⊗(B⊗(C⊗(D⊗E)))=v.

3.1L1step 2.1∎

The composite of steps 1.1 and 2.1 is therefore a canonical map u→v. Any other chain of associators with the same endpoints is equal to it by [L1].

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The word category on words of length three

Example

Among the unit-free binary words of length three, there are exactly two objects: ((−□−)□−),(−□(−□−)).

Facts & Assumptions

Given: The binary-word category W.

[L1]

Binary words are built recursively from e0, (−), and □, with length determined additively (The category of binary words).

[L2]

The category W is monoidal and therefore has the unique structural arrows between equal-length bracketings (The category of binary words is monoidal).

Verification

technique · direct
1.1givenL1

A unit-free length-three word must be obtained by combining exactly three copies of (−) with two binary operations. Up to the placement of brackets, the only possibilities are ((−□−)□−) and (−□(−□−)). Words of length three containing one or more copies of e0 also exist, but are outside this unit-free subcollection.

1.2L1L2

These two words have the same length, so there is exactly one morphism between them in each direction. In the monoidal structure of [L2], those are the associator and its inverse at the generator.

2.1step 1.1step 1.2∎

Thus the unit-free part of the length-three slice of W is the basic coherence picture: two bracketings and one canonical comparison each way.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Strictification of a cartesian monoidal category computed

Example

Let C be a category with finite products, so that C is monoidal under × by A category with finite products is monoidal. Its strictification sends an object X to the endofunctor X×−.

Facts & Assumptions

Given: A category C with finite products.

[L1]

Finite products make C into a monoidal category with tensor × (A category with finite products is monoidal).

[L2]

Strictification sends X to the right-module endofunctor X⊗− and is monoidally equivalent to a strict monoidal category (Mac Lane strictification).

Verification

technique · direct
1.1L1L2

By [L1], the tensor product is ×, so the strictification formula from [L2] becomes L(X)(Y)=X×Y. Its right-module structure map at (Y,Z) is the cartesian associator (X×Y)×Z→X×(Y×Z).

2.1step 1.1L2

The binary comparison L(X)⊗L(Y)⇒L(X×Y) therefore has component the inverse reassociation X×(Y×Z)→(X×Y)×Z, and the unit comparison is Z→1×Z.

3.1step 2.1∎

So in the cartesian case the abstract strictification is completely explicit: it packages ordinary reassociation maps of products into a strict monoidal category of endofunctors.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Two formally distinct words can become the same object

Counterexample

Let M be the one-object category with object ∗ and endomorphism monoid {1,u}, where u≠1 and u2=u. Define the tensor on objects by ∗⊗∗=∗ and on morphisms by the same monoid multiplication. Then M is a strict monoidal category in which the formal words x and (x⊗1) evaluate to the same object ∗.

Facts & Assumptions

Given: The one-object strict monoidal category M just described.

[L1]

In a strict monoidal category, the associator and unitors are identities, so x and (x⊗1) evaluate to the same object on the nose (Strict monoidal category).

[L2]

The slogan "every diagram commutes" fails because formally different vertices can coincide and then a noncanonical endomorphism may be inserted (Why 'every diagram commutes' is false as stated).

Verification

technique · counterexample
1.1L1

By [L1], the two formal vertices x and (x⊗1) both evaluate to the single object ∗ of M.

1.2given

Consider the square all of whose vertices are ∗, whose top edge is u, and whose other three edges are 1. The clockwise composite is u, while the counterclockwise composite is 1, so the square does not commute because u≠1.

2.1L2step 1.1step 1.2∎

This realizes the mechanism described in [L2]: formally distinct words can collapse to one object, and a noncanonical endomorphism then breaks the blanket slogan. Hence the slogan is false.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

A monoid object written with and without associators

Example

Let (M,μ,η) be a monoid object in a monoidal category. Its associativity axiom can be displayed either with explicit bracket-changing data or with the unbracketed shorthand licensed by coherence.

Facts & Assumptions

Given: A monoid object (M,μ,η).

[L1]

The definition of monoid object writes the associativity and unit diagrams with explicit associator and unitor morphisms (Monoid objects and comonoid objects in a monoidal category).

[L2]

After coherence, those axioms may be written without explicit associators (The monoid-object axioms may be written without associators).

Verification

technique · direct
1.1L1

The explicit associativity axiom is μ∘(μ⊗1M)=μ∘(1M⊗μ)∘αM,M,M, and the unit axioms are μ∘(η⊗1M)=λM and μ∘(1M⊗η)=ρM.

1.2L2

By [L2], the same relations may be written as μ(μ⊗1M)=μ(1M⊗μ) and μ(η⊗1M)=1M=μ(1M⊗η), with the bracket suppressions understood canonically.

2.1step 1.1step 1.2∎

Thus the two notations express the same monoid-object structure; the second is shorter only because coherence has already absorbed the bracket changes.

Sources