transport_E'_V_E' {i j : G} (g : G i j) (x : D i) (y : E (i; x)) : transport_E' g x y = ap (transport E' (colimp i j g x)) (transport_E'_V g x y)^ @ transport_pV E' (colimp i j g x) y. Proof. rewrite moveR_transport_V_V, inv_V. symmetry; apply ap_transport_transport_pV. 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.