{A B C : Group} {i : A $-> B} {f : B $-> C} (cx : IsComplex i f) : GroupHomomorphism A (grp_kernel f) := grp_kernel_corec _ cx.
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.