(b : B) : ap cyl_cylcoeq (cglue b) = cglue (cyl b). Proof. etransitivity. 1:rapply functor_coeq_beta_cglue. exact (concat_p1 _ @ concat_1p _). Defined.
Require Import HoTT.Basics Cubical.DPath Cubical.PathSquare. Require Import Colimits.Pushout.