(m : forall y, DiagramMap (D1 y) (D2 y)) : DiagramMap (sigma_diagram D1) (sigma_diagram D2). Proof. srapply Build_DiagramMap. - intros i. srapply (functor_sigma idmap _). intros y; apply m. - intros i j g x; simpl in *. srapply path_sigma'. 1: reflexivity. simpl. apply (DiagramMap_comm (m x.1)). Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cocone. Require Import Colimits.Colimit.