Cocone (parallel_pair f g) (Coeq f g). Proof. srapply Build_Cocone. + intros []; [exact (coeq o g)| exact coeq]. + intros i j phi x; destruct i, j, phi; simpl; [ exact (cglue x) | reflexivity ]. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.ParallelPair. Require Import Diagrams.Cocone. Require Import Colimits.Colimit. Require Import Colimits.Coeq.