{X Y : Group} (f : X $-> Y) : IsComplex (grp_trivial_rec X) f. Proof. srapply phomotopy_homotopy_hset. intro x; cbn. exact (grp_homo_unit f). Defined.
Require Import Basics Types. Require Import Truncations.Core. Require Import WildCat.Core Pointed. Require Import Groups.Group Groups.Subgroup Groups.Kernel. Require Import Homotopy.ExactSequence Modalities.Identity.