{X : Type} (P : Susp X -> Type) (H_N : P North) (H_S : P South) (H_merid : forall x:X, (merid x) # H_N = H_S) : forall (y : Susp X), P y. Proof. srapply Pushout_ind. - exact (Unit_ind H_N). - exact (Unit_ind H_S). - exact (H_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.