(Susp_ind_inv X (P o functor_susp f)) o functor_Susp_ind_type $=> functor_Susp_ind_data o (Susp_ind_inv Y P). Proof. intros g; exists idpath; intros x. change (apD (fun x0 : Susp X => g (functor_susp f x0)) (merid x) = (functor_Susp_ind_data (Susp_ind_inv Y P g)).2 x). refine (dp_apD_compose (functor_susp f) P (merid x) g @ _). cbn; apply ap. apply (moveL_transport_V (fun p => DPath P p (g North) (g South))). exact (apD (apD g) (functor_susp_beta_merid f x)). 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.