(n : nat) (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. induction n in Aa, Pp, istrunc_Pp |- *. { snrapply Build_pEquiv'. 1: refine (@equiv_sigma_contr _ _ istrunc_Pp). reflexivity. } 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.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Factorization Truncations.Core Truncations.Connectedness HProp. Require Import Pointed.Core Pointed.pEquiv. Require Import WildCat. Require Import Spaces.Nat.Core.