(A : Sequence) := { fibSequence : sig A -> Type; fibSequenceArr x : fibSequence x -> fibSequence x^++ }.
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.