fact: Definition functor_susp_beta_merid {X Y : Type} (f : X -> Y) (x : X) : ap (functor_susp f) (merid x) = merid (f x).
imports: Basics Types Cubical WildCat Colimits.Pushout NullHomotopy Truncations.Core Modalities.Modality Extensions