{X Z Y Y' : Group} (f : X $-> Z) (g' : Y' $-> Y) (g : Y $-> Z) : GroupIsomorphism (grp_pullback (grp_pullback_pr2 f g) g') (grp_pullback f (g $o g')). Proof. srapply Build_GroupIsomorphism. - srapply grp_pullback_corec. + exact (grp_pullback_pr1 _ _ $o grp_pullback_pr1 _ _). + apply grp_pullback_pr2. + intro x; cbn. exact (pullback_commsq _ _ _ @ ap g (pullback_commsq _ _ _)). - srapply isequiv_adjointify. + srapply grp_pullback_corec. * srapply functor_grp_pullback. 1,2: exact grp_homo_id. 1: exact g'. all: reflexivity. * apply grp_pullback_pr2. * reflexivity. + intro x; cbn. by srapply equiv_path_pullback_hset. + intros [[x [y z0]] [y' z1]]; srapply equiv_path_pullback_hset; split; cbn. 2: reflexivity. srapply equiv_path_pullback_hset; split; cbn. 1: reflexivity. exact z1^. Defined.
Require Import Basics Types Limits.Pullback Cubical.PathSquare. Require Import Algebra.Groups.Group. Require Import WildCat.Core.