Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `Concatenation with values`

groundedproofs/Lax149335Proofs/Results/Preliminaries.lean · lax-149335

What this proof establishes

no assumptions

lem✓Lax149335.ValueConcatenation

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Each law is derived from the monoid axioms for binconcatbinconcat (Axiom 10) and the coherence laws for products, which in turn follow from Mac Lane's pentagon and triangle.