proposition: Lemma loops_psigma_trunc (n : nat) : forall (Aa : pType) (Pp : pFam Aa) (istrunc_Pp : IsTrunc_pFam (trunc_index_inc minus_two n) Pp), iterated_loops n (psigma Pp) <~>* iterated_loops n Aa.
proof: Proof. induction n. { intros A P p. snrapply Build_pEquiv'. 1: refine (@equiv_sigma_contr _ _ p). reflexivity. } intros A P p. refine (pequiv_inverse (unfold_iterated_loops' _ _) o*E _ o*E unfold_iterated_loops' _ _). refine (IHn _ _ _ o*E _). rapply (emap (iterated_loops _)). apply loops_psigma_commute. Defined.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core