`{Univalence} (A : Type) `{merely A} (p : forall (x y:A), merely (x = y)) : IsConnected 0 A. Proof. strip_truncations. apply contr_inhabited_hprop. - apply hprop_allpath; intros z w. strip_truncations. exact (equiv_path_Tr z w (p z w)). - apply tr; assumption. Defined.
Require Import Basics. Require Import Types. Require Import Extensions. Require Import Factorization. Require Import Modalities.Descent. Require Import Truncations.Core Truncations.SeparatedTrunc.