{X : Type} {P : Susp X -> Type} (f : forall y, P y) : f == Susp_ind P (f North) (f South) (fun x => apD f (merid x)). Proof. unfold pointwise_paths. refine (Susp_ind _ 1 1 _). intros x. refine (transport_paths_FlFr_D (g := Susp_ind P (f North) (f South) (fun x : X => apD f (merid x))) _ _ @ _); simpl. apply moveR_pM. apply equiv_p1_1q. apply ap, inverse. refine (Susp_ind_beta_merid _ _ _ _ _). 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.