fact: Definition merely_path_is0connected `{Univalence} (A : Type) `{IsConnected 0 A} (x y : A) : merely (x = y).
imports: Basics Types Extensions Factorization Modalities.Modality Modalities.Descent Truncations.Core Truncations.SeparatedTrunc