{X : Group} (b : X $-> B) (c : X $-> C) (p : f o b == g o c) : X $-> grp_pullback. Proof. snrapply Build_GroupHomomorphism. - exact (fun x => (b x; c x; p x)). - intros x y. srapply path_sigma. + simpl. apply (grp_homo_op b). + unfold pr2. refine (transport_sigma' _ _ @ _). unfold pr1. apply path_sigma_hprop. simpl. apply (grp_homo_op c). Defined.
Require Import Basics Types Limits.Pullback Cubical.PathSquare. Require Import Algebra.Groups.Group. Require Import WildCat.Core.