{ua : Univalence} {A B : Type} {f : A -> B} (n : trunc_index) {H0 : IsTrunc n A} {H1 : IsTrunc n B} {i : IsEquiv (Trunc_functor 0 f)} {ii : forall (x : A) (k : nat), IsEquiv (fmap (Pi k.+1) (pmap_from_point f x)) } : IsEquiv f. Proof. revert A B H0 H1 f i ii. induction n as [|n IHn]. 1: intros; apply isequiv_contr_contr. intros A B H0 H1 f i ii. nrefine (@isequiv_isbij_tr0_isequiv_loops ua _ _ f i _). intro x. nrefine (isequiv_homotopic (@ap _ _ f x x) _). 2:{intros p; cbn. symmetry; exact (concat_1p _ @ concat_p1 _). } pose proof (@istrunc_paths _ _ H0 x x) as h0. pose proof (@istrunc_paths _ _ H1 (f x) (f x)) as h1. nrefine (IHn (x=x) (f x=f x) h0 h1 (@ap _ _ f x x) _ _). - pose proof (ii x 0) as h2. unfold is0functor_pi in h2; cbn in h2. refine (@isequiv_homotopic _ _ _ _ h2 _). apply (O_functor_homotopy (Tr 0)); intros p. exact (concat_1p _ @ concat_p1 _). - intros p k; revert p. assert (h3 : forall (y:A) (q:x=y), IsEquiv (fmap (Pi k.+1) (pmap_from_point (@ap _ _ f x y) q))). 2:exact (h3 x). intros y q. destruct q. snrefine (isequiv_homotopic _ _). 1: exact (fmap (Pi k.+1) (fmap loops (pmap_from_point f x))). 2:{ rapply (fmap2 (Pi k.+1)); srefine (Build_pHomotopy _ _). - intros p; cbn. refine (concat_1p _ @ concat_p1 _). - reflexivity. } nrefine (isequiv_commsq _ _ _ _ (fmap_pi_loops k.+1 (pmap_from_point f x))). 2-3:refine (equiv_isequiv (pi_loops _ _)). exact (ii x k.+1). 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.