Susp_ind_type Y P -> Susp_ind_type X (P o functor_susp f) := fun g => g o functor_susp f. Local Instance is0functor_functor_Susp_ind_type : Is0Functor . Proof. constructor. intros g h p a. exact (p (functor_susp f a)). 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.