proposition: Theorem equiv_istrunc_contr_iterated_loops `{Funext} (n : nat) : forall A, IsTrunc n.-1 A <~> forall a : A, Contr (iterated_loops n [A, a]).
proof: Proof. induction n; intro A. { cbn. exact equiv_hprop_inhabited_contr. } refine (_ oE equiv_istrunc_istrunc_loops n.-2 _). srapply equiv_functor_forall_id. intro a. cbn beta. refine (_ oE IHn (loops [A, a])). refine (equiv_inO_equiv (-2) (unfold_iterated_loops' n [A,a])^-1 oE _). rapply equiv_iff_hprop. intros X p. refine (@contr_equiv' _ _ _ X). rapply (emap (iterated_loops _)). srapply Build_pEquiv'. 1: exact (equiv_concat_lr p 1). cbn; unfold ispointed_loops. exact (concat_p1 _ @ concat_p1 _). Defined.
imports: HoTT.Basics HoTT.Types HFiber Factorization Truncations.Core Truncations.Connectedness HProp Pointed.Core Pointed.pEquiv WildCat Spaces.Nat.Core