`{Univalence} (n : nat) {X Y : pType} (f : X ->* Y) {C : IsConnMap n f} : IsConnMap (Tr (-1)) (fmap (pPi n.+1) f). Proof. rapply conn_map_O_functor_strong_leq. by apply issurj_iterated_loops_connmap. Defined.
Require Import Basics Types Pointed HSet. Require Import Modalities.Modality. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.AbGroups. Require Import WildCat.