Cyl f -> Cyl f'. Proof. srapply Cyl_rec. - exact (cyl o ga). - exact (cyr o gb). - intros a. refine (_ @ ap cyr (g a)). exact (cyglue (ga a)). Defined.
Require Import HoTT.Basics Cubical.DPath Cubical.PathSquare. Require Import Colimits.Pushout.