{A B Q} {f g : B -> A} `(q: A -> Q) (Hq: q o g == q o f) : Cocone (parallel_pair f g) Q. Proof. srapply Build_Cocone. 1: intros []; [exact (q o f) | exact q]. intros [] [] []; [reflexivity | exact Hq]. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram. Require Import Diagrams.Cocone.