Coeq_ind_inv f g (P o functor_coeq h k p q) o functor_Coeq_ind_type $=> functor_Coeq_ind_data o (Coeq_ind_inv f' g' P). Proof. intros m. exists (fun _ => idpath). intros b; simpl. lhs nrapply concat_1p; rhs nrapply concat_p1. rhs nrapply (dp_apD_compose' _ _ (functor_coeq_beta_cglue h k p q b) _). nrapply ap. nrefine (_ @ (dp_apD_pp _ _ _ _ _)^). rhs nrapply (dp_whiskerR _ (dp_apD_pp _ _ _ _ _)). lhs nrapply (dp_whiskerL _ (dp_apD_compose_inv _ _ _)^). exact (dp_whiskerR _ (dp_whiskerR _ (dp_apD_compose_inv _ _ _)^)). 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.