`{Funext} (U : HProp) : Disjoint (Op U) (Cl U). Proof. intros A. change ((U -> Contr A) -> Contr (U -> A)); intros uc. apply (Build_Contr _ (fun u => let i := uc u in center A)). intros f; apply path_arrow; intros u. pose (uc u); apply path_contr. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Limits.Pullback. Require Import Modality Lex Open Closed Nullification.