(X : pType) : ooGroup. Proof. pose (BG := [{ x:X & merely (x = pt) }, exist (fun x:X => merely (x = pt)) pt (tr 1)]). cut (IsConnected 0 BG). { exact (Build_ooGroup BG). } cut (IsSurjection (unit_name (point BG))). { intros; refine (conn_pointed_type pt). } apply BuildIsSurjection; simpl; intros [x p]. strip_truncations; apply tr; exists tt. apply path_sigma_hprop; simpl. exact (p^). 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.