`{Univalence} {A B : Type} (f : A -> B) {i : IsEquiv (Trunc_functor 0 f)} {ii : forall x, IsEquiv (fmap loops (pmap_from_point f x)) } : IsEquiv f. Proof. srapply (isequiv_issurj_tr0_isequiv_ap f). intros x y. apply isequiv_inhab_codomain. intro p. apply (ap (@tr 0 _)) in p. apply (@equiv_inj _ _ _ i (tr x) (tr y)) in p. apply (equiv_path_Tr _ _)^-1 in p. strip_truncations. destruct p. cbn in ii. snrapply (isequiv_homotopic _ (H:=ii x)). exact (fun _ => concat_1p _ @ concat_p1 _). Defined.
Require Import Basics Types. Require Import Pointed. Require Import WildCat.Core HFiber. Require Import Truncations. Require Import Algebra.Groups.Group. Require Import Homotopy.HomotopyGroup.