proposition: Theorem isequiv_grp_pullback_corec (X : Group) : IsEquiv (grp_pullback_corec' f g X).
proof: 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.
imports: Basics Types Limits.Pullback Cubical.PathSquare Algebra.Groups.Group WildCat.Core