proposition: Lemma iscolimit_prod {Q : Type} (HQ : IsColimit D Q) : IsColimit prod_diagram (A * Q).
proof: Proof. eapply iscolimit_postcompose_equiv. - apply equiv_sigma_prod0. - eapply iscolimit_precompose_equiv. + symmetry; apply diagram_equiv_prod_sigma. + by apply iscolimit_sigma. Defined.
imports: Basics Types Diagrams.Diagram Colimits.Colimit Colimits.Colimit_Sigma Diagrams.Graph