{A A' B B' C C' : Group} (f : B $-> A) (f' : B' $-> A') (g : C $-> A) (g' : C' $-> A') (alpha : A $-> A') (beta : B $-> B') (gamma : C $-> C') (h : f' o beta == alpha o f) (k : alpha o g == g' o gamma) : grp_pullback f g $-> grp_pullback f' g'. Proof. srapply grp_pullback_corec. - exact (beta $o grp_pullback_pr1 f g). - exact (gamma $o grp_pullback_pr2 f g). - intro x; cbn. refine (h _ @ ap alpha _ @ k _). apply pullback_commsq. Defined.
Require Import Basics Types Limits.Pullback Cubical.PathSquare. Require Import Algebra.Groups.Group. Require Import WildCat.Core.