colim functor
Definition
Let 
be categories and let 
be the Category FunColimit
Then the colimit functor is defined as covariant functor
where 
is the morphism induced by the universal property
Proof
objects
for each diagram 
, choose a representative of the isomorphism class of colimits.
Uses AC,
identity
Given the identity natural transformation, the identity morphism 
makes the diagram commute.
By universal property, it is the only morphism making the diagram commute, hence by construction we get 
composition
Suppose we have objects 
and natural transformations 
Then we get
where both halfes commute, hence also the whole prim.
Therefore, we get a unique morphism
But the composition 
makes also the diagram commute, hence by uniqueness induced by the universal property, we conclude, that
