{A A' B B' C C' : Group} (f : B $-> A) (f' : B' $-> A') (g : C $-> A) (g' : C' $-> A') (alpha : GroupIsomorphism A A') (beta : GroupIsomorphism B B') (gamma : GroupIsomorphism C C') (h : f' o beta == alpha o f) (k : alpha o g == g' o gamma) : GroupIsomorphism (grp_pullback f g) (grp_pullback f' g'). Proof. srapply Build_GroupIsomorphism. 1: exact (functor_grp_pullback f f' g g' _ _ _ h k). srapply isequiv_adjointify. { srapply (functor_grp_pullback f' f g' g). 1-3: rapply grp_iso_inverse; assumption. + rapply (equiv_ind beta); intro b. refine (ap f (eissect _ _) @ _). apply (equiv_ap' alpha _ _)^-1. exact ((h b)^ @ (eisretr _ _)^). + rapply (equiv_ind gamma); intro c. refine (_ @ ap g (eissect _ _)^). apply (equiv_ap' alpha _ _)^-1. exact (eisretr _ _ @ (k c)^). } all: intro x; apply equiv_path_pullback_hset; split; cbn. 1-2: apply eisretr. 1-2: apply eissect. Defined.
Require Import Basics Types Limits.Pullback Cubical.PathSquare. Require Import Algebra.Groups.Group. Require Import WildCat.Core.