CoreflectiveSubuniverse. Proof. simple refine (Build_CoreflectiveSubuniverse (fun X => Build_HProp (X -> U)) (fun X => X * U) (fun X => @snd X U) (fun X => @fst X U) _); try exact _. intros Y X YU; simpl in *. refine (isequiv_adjointify _ (fun h y => (h y , YU y)) _ _). - intros g; apply path_arrow; intros y; reflexivity. - intros h; apply path_arrow; intros y. apply path_prod; [ reflexivity | by apply path_ishprop ]. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Modalities.Modality Modalities.Open.