proposition: Lemma grp_pullback_corec_pr2 {X : Group} (b : X $-> B) (c : X $-> C) (p : f o b == g o c) : grp_pullback_pr2 f g $o grp_pullback_corec f g b c p = c.
proof: Proof. apply equiv_path_grouphomomorphism; reflexivity. Defined.
imports: Basics Types Limits.Pullback Cubical.PathSquare Algebra.Groups.Group WildCat.Core