{i j : G} (g : G i j) (x : D i) (y : E (i; x)) : transport E' (colimp i j g x)^ y = E_f g x y. Proof. apply moveR_transport_V. symmetry. apply transport_E'. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cocone. Require Import Diagrams.DDiagram. Require Import Colimits.Colimit.