fact: Definition isequiv_issurj_tr0_isequiv_ap `{Univalence} {A B : Type} (f : A -> B) {i : IsSurjection (Trunc_functor 0 f)} {ii : forall x y, IsEquiv (@ap _ _ f x y)} : IsEquiv f.
imports: Basics Types Pointed WildCat.Core HFiber Truncations Algebra.Groups.Group Homotopy.HomotopyGroup