The Seifert-van Kampen theorem computes the fundamental group of a space from the fundamental groups of its constituents. We formalize this theorem within the framework of computational paths -- an approach to equality where witnesses are explicit sequences of rewrites governed by the confluent, terminating LND_EQ-TRS. Our contributions are: (i) pushouts as higher-inductive types with explicit path constructors; (ii) free products and amalgamated free products as quotients of word representations; (iii) an encode-decode proof establishing pi_1(Pushout(A,B,C)) = pi_1(A) *_{pi_1(C)} pi_1(B); and (iv) applications to the figure-eight (pi_1(S^1 V S^1) = Z * Z), 2-sphere (pi_1(S^2) = 1), and 3-sphere (pi_1(S^3) = 1 with Hopf fibration context). Recent extensions include: higher homotopy groups pi_n via the weak omega-groupoid structure (with pi_2 abelian via Eckmann-Hilton, and pi_2 = 1 in the 1-groupoid truncated setting); truncation levels connecting the framework to HoTT n-types; automated path simplification tactics; basic covering space theory with pi_1-actions on fibers; fibration theory with long exact sequences; and Eilenberg-MacLane space characterization (S^1 = K(Z,1)). The framework makes coherence witnesses explicit as rewrite derivations. The development is formalized in Lean 4 with over 25,000 lines of mechanized proofs. This demonstrates that the encode-decode method for higher-inductive types becomes fully constructive when path equality is decidable via normalization.

翻译：暂无翻译