(U : HProp) : Modality. Proof. snrapply Build_Modality. - intros X; exact (U -> Contr X). - exact _. - intros T B T_inO f feq. cbn; intros u; pose (T_inO u). refine (contr_equiv _ f); exact _. - intros ; exact (Join U X). - intros T u. pose (contr_inhabited_hprop _ u). exact _. - intros T x. exact (push (inr x)). - intros A B B_inO f z. srefine (Pushout_ind B _ _ _ z). + intros u; apply center, B_inO, u. + intros a; apply f. + intros [u a]. pose (B_inO (push (inr a)) u). apply path_contr. - intros; reflexivity. - intros A A_inO z z' u. pose (A_inO u). apply contr_paths_contr. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import Modality Accessible Nullification Lex Topological. Require Import Colimits.Pushout Homotopy.Join.Core.