sig (Coeq_ind_data f' g' P) -> sig (Coeq_ind_data f g (P o functor_coeq h k p q)). Proof. intros [m r]. exists (m o k). intros b. unfold Coeq_ind_data in r. apply (dp_compose' _ _ (functor_coeq_beta_cglue h k p q b)). nrefine (_ @Dp r (h b) @Dp _). 1: exact (dp_compose coeq P (p b) (apD m (p b))). exact (dp_compose coeq P (q b)^ (apD m (q b)^)). Defined.
Require Import Basics.Overture. Require Import Basics.Tactics. Require Import Basics.PathGroupoids. Require Import Types.Paths. Require Import Colimits.Coeq. Require Import Cubical.DPath. Require Import Cubical.DPathSquare. Require Import WildCat.Core. Require Import WildCat.Displayed. Require Import WildCat.Equiv. Require Import WildCat.EquivGpd. Require Import WildCat.Forall. Require Import WildCat.NatTrans. Require Import WildCat.Paths. Require Import WildCat.ZeroGroupoid.