(X : pType) : Group. Proof. srapply (Build_Group (Tr 0 (loops X))); repeat split. + intros x y. strip_truncations. exact (tr (x @ y)). + exact (tr 1). + srapply Trunc_rec; intro x. exact (tr x^). + exact _. + intros x y z. strip_truncations. cbn; apply ap. apply concat_p_pp. + intro x. strip_truncations. cbn; apply ap. apply concat_1p. + intro x. strip_truncations. cbn; apply ap. apply concat_p1. + intro x. strip_truncations. apply (ap tr). apply concat_Vp. + intro x. strip_truncations. apply (ap tr). apply concat_pV. Defined.
Require Import Basics Types Pointed HSet. Require Import Modalities.Modality. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.AbGroups. Require Import WildCat.