Group -> ooGroup := fun G => Build_ooGroup (pClassifyingSpace G) _. Global Instance is0functor_group_to_oogroup : Is0Functor . Proof. snrapply Build_Is0Functor. intros G H f. by rapply (fmap pClassifyingSpace). Defined.
Require Import Basics Types. Require Import Pointed. Require Import Truncations.Core Truncations.Connectedness. Require Import Homotopy.ClassifyingSpace. Require Import Algebra.Groups. Require Import WildCat.