(S : Type) : S -> Pi 1 (Bouquet S). Proof. rapply equiv_pi1bouquet_rec. apply grp_homo_id. 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.