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