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