`{Funext} : Modality. Proof. snrapply easy_modality. - intros X; exact (~ (~ X)). - intros T x nx; exact (nx x). - intros A B f z nBz. apply z; intros a. exact (f a (transport (fun x => ~ (B x)) (path_ishprop _ _) nBz)). - intros A B f a. apply path_ishprop. - intros A z z'. refine (isequiv_iff_hprop _ _). intros; apply path_ishprop. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Modality.