`{Funext} (U : HProp) : Modality. Proof. snrapply easy_modality. - intros X; exact (U -> X). - intros T x; cbn. exact (fun _ => x). - cbn; intros A B f z u. refine (transport B _ (f (z u) u)). apply path_arrow; intros u'. apply ap; apply path_ishprop. - cbn; intros A B f a. apply path_arrow; intros u. transitivity (transport B 1 (f a u)); auto with path_hints. apply (ap (fun p => transport B p (f a u))). transitivity (path_arrow (fun _ => a) (fun _ => a) (@ap10 U _ _ _ 1)); auto with path_hints. * apply ap. apply path_forall; intros u'. apply ap_const. * apply eta_path_arrow. - intros A z z'. srefine (isequiv_adjointify _ _ _ _). * intros f; apply path_arrow; intros u. exact (ap10 (f u) u). * intros f; apply path_arrow; intros u. transitivity (path_arrow z z' (ap10 (f u))). + unfold to; apply ap. apply path_forall; intros u'. apply (ap (fun u0 => ap10 (f u0) u')). apply path_ishprop. + apply eta_path_arrow. * intros p. refine (eta_path_arrow _ _ _). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import Modality Accessible Nullification Lex.