{A : Type} `{IsConnected O A} (x y : A) : IsConnected O (x = y) := OO_isconnected_paths O O x y.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Limits.Pullback Factorization Truncations.Core. Require Import Modality Accessible Modalities.Localization Descent Separated.