`{Univalence} {A} (B : FibSequence A) : Colimit A -> Type. Proof. srapply Colimit_rec; srapply Build_Cocone. - exact (fun n a => Colimit (fib_seq_to_seq B (n;a))). - intros n m p a; destruct p; apply path_universe_uncurried. exact (equiv_colim_succ_seq_to_colim_seq (fib_seq_to_seq B (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.