{X Y Z} (f : X -> Y) (g : Y -> Z) : functor_susp (g o f) == functor_susp g o functor_susp f. Proof. snrapply Susp_ind_FlFr. 1,2: reflexivity. intro x. apply equiv_p1_1q. lhs nrapply functor_susp_beta_merid; symmetry. lhs nrefine (ap_compose (functor_susp f) _ (merid x)). lhs nrefine (ap _ (functor_susp_beta_merid _ _)). apply functor_susp_beta_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.