fact: Definition ap_pr_cylcoeq_cglue (x : Cyl h) : PathSquare (ap pr_cylcoeq (cglue x)) (cglue (pr_cyl x)) (ap coeq (pr_functor_cyl p x)) (ap coeq (pr_functor_cyl q x)).
imports: HoTT.Basics Cubical.DPath Cubical.PathSquare Colimits.Pushout