proposition: Proposition grp_pullback_corec {X : Group} (b : X $-> B) (c : X $-> C) (p : f o b == g o c) : X $-> grp_pullback.
proof: 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.
imports: Basics Types Limits.Pullback Cubical.PathSquare Algebra.Groups.Group WildCat.Core