`{Univalence} (A : Type) `{IsConnected 0 A} (x y : A) : merely (x = y). Proof. rapply center. Defined.
Require Import Basics. Require Import Types. Require Import Extensions. Require Import Factorization. Require Import Modalities.Descent. Require Import Truncations.Core Truncations.SeparatedTrunc.