almost_inSepO_typeO@{i j} `{Univalence} (O : ReflectiveSubuniverse) (A B : Type_@{i j} O) : { Z : Type@{i} & In O Z * (Z <~> (A = B)) }. Proof. exists (A <~> B); split. - exact _. - refine (equiv_path_TypeO O A B oE _). apply equiv_path_universe. Defined.
Require Import HoTT.Basics HoTT.Types HoTT.Cubical.DPath. Require Import HFiber Extensions Factorization Limits.Pullback. Require Import Modality Accessible Descent. Require Import Truncations.Core. Require Import Homotopy.Suspension.