gluable_open_closed' (U : HProp) : Gluable (Op' U) (Cl' U). Proof. intros A ? u; simpl in *. pose proof (contr_inhabited_hprop U u). assert (Contr A). { simple refine (contr_equiv (Op' U A) _). - refine (O_rec idmap). intros []; simpl. apply ooextendable_equiv. refine (equiv_isequiv (@equiv_contr_contr U Unit _ _)). - refine (isequiv_adjointify _ (to (Op' U) A) _ _). + intros a; apply O_rec_beta. + apply O_indpaths; cbn. reflexivity. } apply ooextendable_contr; exact _. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Limits.Pullback. Require Import Modality Lex Open Closed Nullification.