`{Funext} (U : HProp) : Gluable (Op U) (Cl U). Proof. intros A. change (Contr (U -> A) -> (U -> Contr A)); intros ? u. apply (Build_Contr _ (center (U -> A) u)); intros a. exact (ap10 (path_contr _ (fun _ => a)) u). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Limits.Pullback. Require Import Modality Lex Open Closed Nullification.