isequiv_pi_connmap' `{Univalence} (n : nat) {X Y : pType} (f : X ->* Y) `{!IsConnMap n f} : IsEquiv (fmap (pTr 0) (fmap (iterated_loops n) f)). Proof. rapply O_inverts_conn_map. rapply isconnected_iterated_fmap_loops. rewrite 2 trunc_index_inc'_succ. rewrite <- trunc_index_inc_agree. assumption. Defined.
Require Import Basics Types Pointed HSet. Require Import Modalities.Modality. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.AbGroups. Require Import WildCat.