IsSurjInj Susp_ind_inv. Proof. constructor. - intros [[n s] g]. exists (Susp_ind P n s g); cbn. exists idpath. intros x; cbn. apply Susp_ind_beta_merid. - intros f g [p q]; cbn in *. srapply Susp_ind; cbn. 1: exact (ap fst p). 1: exact (ap snd p). intros x; specialize (q x). apply ds_dp. apply ds_transport_dpath. rewrite transport_forall_constant in q. rewrite <- (eta_path_prod p) in q. rewrite transport_path_prod in q. exact q. Defined.
Require Import Basics. Require Import Types. Require Import Cubical.DPath Cubical.DPathSquare. Require Import WildCat. Require Import Colimits.Pushout. Require Import NullHomotopy. Require Import Truncations.Core. Require Import Modalities.Modality. Require Import Extensions.