`{Univalence} {A} (B : FibSequence A) : Colimit (sig_seq B) -> sig (fib_seq_to_type_fam B). Proof. srapply Colimit_rec; srapply Build_Cocone. - intros n [a b]; exact (inj A n a; inj (fib_seq_to_seq _ _) 0 b). - intros n m p [a b]; destruct p; srefine (_ @ ap _ (glue (fib_seq_to_seq _ _) 0 b)). srapply (Delta _ (fib_seq_to_type_fam_beta_glue 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.