{A} (B : FibSequence A) (x : sig A) : Sequence. Proof. srapply Build_Sequence; intro k; revert x; induction k as [ | k h]. * exact (fun x => B x). * exact (fun x => h x^++). * exact (fun x b => b^+f). * exact (fun x => h x^++). 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.