{X Y : Type} (f : Susp X -> Y) : f == Susp_rec (f North) (f South) (fun x => ap f (merid x)). Proof. snrapply Susp_ind_FlFr. 1, 2: reflexivity. intro x. apply equiv_p1_1q. exact (Susp_rec_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.