Proof of `The bundle lemma`
groundedproofs/Lax149335Proofs/Results/SimpleCompleteness.lean · lax-149335
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
For binary strings and bundles of size two, the window axiom provides the inverse of the concatenation map. Every type is a retract of the binary strings, by Lemma 5.6, and concatenation maps are natural, which gives bundles of size two for every type. Bundles of bundles multiply the bundle sizes, which gives all powers of two.