disjoint_open_closed' (U : HProp) : Disjoint (Op' U) (Cl' U). Proof. intros A An. apply isconnected_from_elim; intros C Cn f. simple refine (@local_rec _ C Cn tt _ tt ; _); simpl. - intros u. exact (f (@local_rec _ A An u Empty_rec tt)). - intros a; simpl. refine (@local_indpaths _ C Cn tt (fun _ => f a) _ _ tt); intros u; simpl in *. refine (_ @ (@local_rec_beta _ C Cn tt _ u)^). apply ap. exact (@local_indpaths _ A An u (fun _ => a) _ (Empty_ind _) tt). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Limits.Pullback. Require Import Modality Lex Open Closed Nullification.