A n : Colimit (shift_seq A n) -> Colimit A. Proof. srapply Colimit_rec; srapply Build_Cocone. + exact (fun k a => inj A (k+n)%nat a). + intros k l p; destruct p; exact (glue A (k+n)%nat). Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.Sequence. Require Import Diagrams.Cocone. Require Import Colimits.Colimit. Require Import Spaces.Nat.Core. Require Import Homotopy.IdentitySystems.