(a : A) : pr_functor_cyl (cyl a) = g a. Proof. refine (ap _ (inv_V _) @ _). refine (ap_compose functor_cyl pr_cyl (cyglue a) @ _). refine (ap _ (ap_functor_cyl_cyglue a) @ _). refine (ap_pp _ _ _ @ _). refine (whiskerR (ap_pr_cyl_cyglue (ga a)) _ @ concat_1p _ @ _). refine ((ap_compose cyr _ (g a))^ @ _). apply ap_idmap. Defined.
Require Import HoTT.Basics Cubical.DPath Cubical.PathSquare. Require Import Colimits.Pushout.