`{MapIn O _ _ (diagonal f)} : MapIn (Sep O) f. Proof. intros x1 u v. destruct v as [x2 p]. destruct p. refine (inO_equiv_inO' _ (hfiber_diagonal f (u.1; x2; u.2))). 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.