{X Y : Type} (f g : Susp X -> Y) (HN : f North = g North) (HS : f South = g South) (Hmerid : forall x, ap f (merid x) @ HS = HN @ ap g (merid x)) : f == g. Proof. snrapply Susp_ind. - exact HN. - exact HS. - intro x. nrapply transport_paths_FlFr'. apply Hmerid. 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.