Susp_ind_data'' (NS : P North * P South) := forall x:X, DPath P (merid (f x)) (fst NS) (snd NS). Local Instance isgraph_Susp_ind_data'' NS : IsGraph (Susp_ind_data'' NS). Proof. apply isgraph_forall; intros; apply isgraph_paths. 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.