`{Univalence} {A} (B : FibSequence A) : pr1 o (seq_colim_sum_to_sum_seq_colim B) == seq_colim_sum_to_seq_colim_fst B. Proof. srapply seq_colimit_uniq. - exact (fun n a => idpath). - intros n [a b]; rewrite concat_1p, concat_p1, ap_compose, !Colimit_rec_beta_colimp. rewrite ap_pp, (Delta_proj _ (fib_seq_to_type_fam_beta_glue B n a)). srapply (whiskerL _ _ @ concat_p1 _); rewrite (ap_compose _ _ _)^; simpl. rewrite ap_const; reflexivity. 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.