fact: Record ooGroup := { classifying_space : pType ; isconn_classifying_space : IsConnected 0 classifying_space }.
imports: Basics Types Pointed Truncations.Core Truncations.Connectedness Homotopy.ClassifyingSpace Algebra.Groups WildCat