(X : Group) : IsEquiv (grp_pullback_corec' f g X). Proof. snrapply isequiv_adjointify. - intro phi. refine (grp_pullback_pr1 f g $o phi; grp_pullback_pr2 f g $o phi; _). intro x; exact (pullback_commsq f g (phi x)). - intro phi. apply equiv_path_grouphomomorphism; reflexivity. - intro bcp; simpl. srapply path_sigma. + simpl. apply grp_pullback_corec_pr1. + refine (transport_sigma' _ _ @ _). apply path_sigma_hprop; simpl pr1. simpl. apply grp_pullback_corec_pr2. Defined.
Require Import Basics Types Limits.Pullback Cubical.PathSquare. Require Import Algebra.Groups.Group. Require Import WildCat.Core.