{X Y} {f g : X -> Y} (h : f == g) : functor_susp f == functor_susp g. Proof. srapply Susp_ind_FlFr. 1, 2: reflexivity. intro x. apply equiv_p1_1q. lhs nrapply (functor_susp_beta_merid f). rhs nrapply (functor_susp_beta_merid g). apply ap, h. 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.