functor_coeq h k p q == pr_cylcoeq o cyl_cylcoeq. Proof. intros c. refine (_ @ functor_coeq_compose cyl cyl (functor_cyl_cyl p) (functor_cyl_cyl q) pr_cyl pr_cyl (pr_functor_cyl p) (pr_functor_cyl q) c). srapply functor_coeq_homotopy. 1-2:reflexivity. all:intros b; cbn. all:refine (concat_1p _ @ concat_1p _ @ _ @ (concat_p1 _)^). all:apply pr_functor_cyl_cyl. Defined.
Require Import HoTT.Basics Cubical.DPath Cubical.PathSquare. Require Import Colimits.Pushout.