transport_E' {i j : G} (g : G i j) (x : D i) (y : E (i; x)) : transport E' (colimp i j g x) (E_f g x y) = y. Proof. refine (transport_idmap_ap _ _ _ @ _). srefine (transport2 idmap _ _ @ _). 2: apply Colimit_rec_beta_colimp; cbn. apply (moveR_transport_V idmap). symmetry; apply transport_path_universe. 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.