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