`{O' <= Sep O} {X : Type@{i}} (x y : X) : O (x = y) -> (to O' X x = to O' X y). Proof. nrefine (O_rec (O := O) (@ap X (O' X) (to O' X) x y)). - rapply (@inO_leq O' (Sep O)). - exact _. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.