Coeq_ind_type -> sig Coeq_ind_data. Proof. intros h. exists (h o coeq). intros b. exact (apD h (cglue 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.