{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. apply equiv_path_grouphomomorphism; reflexivity. Defined.
Require Import Basics Types Limits.Pullback Cubical.PathSquare. Require Import Algebra.Groups.Group. Require Import WildCat.Core.