forall z:Susp X, P z. Local Instance isgraph_Susp_ind_type : IsGraph . 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.