(X : pType) : loops X <~> group_loops X. Proof. unfold loops, group_type. simpl. exact (equiv_path_sigma_hprop (point X ; tr 1) (point X ; tr 1)). 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.