A : Colimit (succ_seq A) -> Colimit A. Proof. srapply Colimit_rec; srapply Build_Cocone. + exact (fun n a => inj _ n.+1 a). + intros n m p; destruct p; exact (glue A n.+1). 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.