{A} (B : FibSequence A) : Sequence. Proof. srapply Build_Sequence. - exact (fun n => {a : A n & B (n;a)}). - intros n [a b]; exact (a^+; b^+f). 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.