proposition: Theorem equiv_pi1bouquet_rec (S : Type) (G : Group) : (Pi 1 (Bouquet S) $-> G) <~> (S -> G).
proof: Proof. apply natequiv_pi1bouquet_rec. Defined.
imports: Basics Types Pointed WildCat Algebra.Groups Modalities.ReflectiveSubuniverse Truncations.Core Homotopy.Suspension Homotopy.ClassifyingSpace Homotopy.HomotopyGroup