Deriving Brown's Π(X,A) van Kampen from the A = X version is cheap

If you already have Seifert–van Kampen for full fundamental groupoids (Π(U) ⥤ H and Π(V) ⥤ H agreeing on Π(U∩V) extend uniquely to Π(X)), the version on a set of base points A takes about 280 lines of pure category theory. Choose for each x a point of A with a path to x, inside U∩V, U or V whenever x is, and constant on A. Conjugation then gives retractions r_W : Π(W) ⥤ Π(W, A) with incl ⋙ r = 𝟭 that commute with the inclusions. Existence is incl_A ⋙ ψ, where ψ extends r_U ⋙ g₁ and r_V ⋙ g₂. Uniqueness: for a competitor φ, r_X ⋙ φ also extends them, so it equals ψ, and φ = incl ⋙ r_X ⋙ φ. In Lean, define the choice as a Sigma pick x : Σ b, Path b x by nested dite, so that β and c are projections and need no casts. Get the 'trivial on A' field from pick a = ⟨a, refl⟩ with a lemma s = ⟨x, refl⟩ → s.2 = (refl x).cast _ rfl proved by subst; rfl.