A / grp_kernel phi $-> grp_image phi. Proof. srapply grp_quotient_rec. + srapply grp_image_in. + intros n x. by apply path_sigma_hprop. Defined.
Require Import Basics Types. Require Import Truncations.Core. Require Import Algebra.Congruence. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. Require Import HSet. Require Import Spaces.Finite.Finite. Require Import WildCat. Require Import Modalities.Modality.