{A} (B : FibSequence A) : Colimit (sig_seq B) -> Colimit A. Proof. srapply Colimit_rec; srapply Build_Cocone. - intros n [a _]; exact (inj _ n a). - intros n m p [a b]; destruct p; exact (glue _ n a). 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.