`{Univalence} (n : trunc_index) (k : nat) (A B : pType) (f : A ->* B) (C : IsConnMap (trunc_index_inc' n k) f) : IsConnMap n (fmap (iterated_loops k) f). Proof. induction k in n, C |- *. - exact C. - apply isconnected_fmap_loops. apply IHk. exact C. 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.