(S : Type) : NatEquiv (opyon (Pi 1 (Bouquet S))) (opyon S o group_type). Proof. nrefine (natequiv_compose _ _). 1: refine (natequiv_prewhisker (natequiv_pointify_r S) ptype_group). nrefine (natequiv_compose _ _). 1: rapply (natequiv_postwhisker _ (natequiv_inverse natequiv_g_loops_bg)). nrefine (natequiv_compose _ _). 1: refine (natequiv_prewhisker (natequiv_loop_susp_adjoint_r (pointify S)) B). rapply natequiv_bg_pi1_adjoint. 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.