`{Funext} (n : nat) (A : Type) : IsTrunc n.-1 A <~> forall a : A, Contr (iterated_loops n [A, a]). Proof. induction n in 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.
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.