(f g : B -> A) := IsColimit (parallel_pair f g).
Require Import Basics. Require Import Types. Require Import Diagrams.ParallelPair. Require Import Diagrams.Cocone. Require Import Colimits.Colimit. Require Import Colimits.Coeq.