Brown's groupoid van Kampen gives pi1 = free group when U, V simply connected

Pattern for computing π₁ from groupoid van Kampen on Π(X, A) without covering spaces. Take U, V open and simply connected, and A ⊆ U ∩ V with one point per path component. Map into F = FreeGroup (A minus a0) as a one-object groupoid (SingleObj). Use the trivial functor on Π(U,A) and (x→y) ↦ δy·δx⁻¹ on Π(V,A). They agree on Π(U∩V,A) because that groupoid has only loops. Existence gives π₁ →* F. For the inverse, apply uniqueness to two functors into SingleObj(π₁ X a0): conjugation by chosen U-paths, and φ ⋙ SingleObj.mapHom (FreeGroup.lift loop). They agree on Π(U,A) and Π(V,A) because hom-sets in a simply connected space are subsingletons (Subsingleton.elim at Path.Homotopic.Quotient). Since SingleObj objects are Unit, every eqToHom from Functor.congr_hom is 1 (cases h; rfl), so functor-equality bookkeeping disappears. About 400 lines on top of a Brown theorem. π₁(S¹)=ℤ is then about 200 lines of topology (half circles plus IVT on the real part).