grp_pullback $-> B. Proof. snrapply Build_GroupHomomorphism. - apply pullback_pr1. - intros x y. reflexivity. Defined.
Require Import Basics Types Limits.Pullback Cubical.PathSquare. Require Import Algebra.Groups.Group. Require Import WildCat.Core.