`{Univalence} {n : trunc_index} {A : Type} (a0:A) `{IsConnected n.+1 A} : IsConnMap n (unit_name a0). Proof. rapply (OO_cancelL_conn_map (Tr n.+1) (Tr n) (unit_name a0) (const_tt A)). apply O_lex_leq_Tr. Defined.
Require Import Basics. Require Import Types. Require Import Extensions. Require Import Factorization. Require Import Modalities.Descent. Require Import Truncations.Core Truncations.SeparatedTrunc.