(S : Type) : pType := psusp (pointify S). Global Instance isconnected_bouquet (S : Type) : IsConnected 0 ( S). Proof. rapply isconnected_susp. 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.