(m : forall y, (D1 y) ~d~ (D2 y)) : (sigma_diagram D1) ~d~ (sigma_diagram D2). Proof. srapply (Build_diagram_equiv (sigma_diagram_functor m)). intros i. srapply isequiv_functor_sigma. intros y; apply m. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cocone. Require Import Colimits.Colimit.