{X Y : Type} (f : X -> Y) (x : X) : ap (functor_susp f) (merid x) = merid (f x). Proof. srapply Susp_rec_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.